Example

       ((a ∨ (a → b)) → b) → b 

1	Assume (a ∨ (a → b)) → b)			Assume we have f :: (Either a (a -> b)) -> b
2	Assume a			Assume we have x :: a
3	From (2), conclude a ∨ (a → b)	(∨I)		Left x	:: Either a (a -> b)
4	From (3) and (1), conclude b	(→E)		f (Left x)	:: b
5	From (2) and (4), conclude a → b	(→I)	(disch. 2)	\x -> f (Left x)	:: a -> b
6	From (5) conclude a ∨ (a → b)	(∨I)		Right (\x -> f (Left x))	:: Either a (a -> b)
7	From (6) and (1), conclude b	(→E)		f (Right (\x -> f (Left x)))	:: b
5	From (1) and (7), conclude (a ∨ (a → b)) → b) → b	(→I)	(disch. 1)	\f -> f (Right (\x -> f (Left x)))	:: ((Either a (a -> b)) -> b) -> b

• If nothing else this should convince you that Haskell types can be surprising