How to construct a function with any type

• The proof rules match the rules for constructing functions!

• Suppose you have a proof of some proposition

• The last step is either →I or →E

• Say it's →E.

• Then we are concluding b from both a → b and a

• So we have proofs of a → b and a

• So we have programs of types a -> b and a

• (Say f :: a -> b and x :: a)

• Then f x :: b