Types Are Theorems; Programs Are Proofs

Example

((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)

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)