Next  Types Are Theorems; Programs Are Proofs  20 
((a → b) ∧ a) → b
1  Assume (a → b) ∧ a  
2  From (1), conclude a → b  (∧E)
 
3  From (1), conclude a  (∧E)
 
4  From (3) and (2), conclude b  (→E)
 
5  From (1) and (4), conclude ((a → b) ∧ a) → b  (→I)  (discharge 1)

Next  Next 