|Next||Types Are Theorems; Programs Are Proofs||15|
Suppose the last step of the proof is →I.
Then we're proving a → b where a was assumed and we proved b
If we had a proof of a we could prove b
So we can write a function that takes an argument of type a
And turns it into a value of type b
\a -> b :: a -> b