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

Next | Next |