How to construct a function with any type

• Here's our proof of (a → b) → (b → c) → (a → c) again:

1	Assume a → b			Assume we have x :: a -> b
2	Assume b → c			Assume we have y :: b -> c
3	Assume a			Assume we have z :: a
4	From (3) and (1), conclude b	(→E)		x z	:: b
5	From (4) and (2), conclude c	(→E)		y (x z)	:: c
6	From (3) and (5), conclude a → c	(→I)	(disch. 3)	\z -> y (x z)	:: a -> c
7	From (2) and (6), conclude (b → c) → (a → c)	(→I)	(disch. 2)	\y -> (\z -> y (x z))	:: (b -> c) -> (a -> c)
8	From (1) and (7), conclude (a → b) → (b → c) → (a → c)	(→I)	(disch. 1)	\x -> \y -> (\z -> y (x z))	:: (a -> b) -> (b -> c) -> (a -> c)