>>12399324Under Curry-Howard, the proof of
is
I.e.
And, more specifically, for your question use this with .
Let me comment on it. Say you want to prove.
The proof is a procedure F which takes a procedure and returns a procedure that takes a procedure and returns a procedure of type .
You can also say function for procedure.
The concatenation does the job.
In words, the proof
reads
given a reason f to believe that p implies q, then given a reason g to believe that q implies r, you can combine them to see that p implies r.
If you want to use your calculus rules to plug this together in steps, you'll only need the first three rules (since none of the above has to do with "and" or "or" and not even really with "bot", since I generalized your claim).
The example in the bottom of your pic also only concerned implications
