Next  Types Are Theorems; Programs Are Proofs  26 
This one is sufficiently complicated that it's not obvious:
((a ∨ (a → b)) → b) → b
1  Assume (a ∨ (a → b)) → b)  
2  Assume a  
3  From (2), conclude a ∨ (a → b)  (∨I)
 
4  From (3) and (1), conclude b  (→E)
 
5  From (2) and (4), conclude a → b  (→I)  (discharge 2) 
6  From (5) conclude a ∨ (a → b)  (∨I)  
7  From (6) and (1), conclude b  (→E)
 
8  From (1) and (7), conclude (a ∨ (a → b)) → b) → b  (→I)  (discharge 1)

Next  Next 