Another proof

1	Assume a
2	Assume b
3	From (2) and (1), conclude b → a	(→I)	(discharges 2)
4	From (1) and (3), conclude a → (b → a)	(→I)	(discharges 1)

• What if we did this instead:

1	Assume a
2	Assume b
3	From (2) and (1), conclude b → a	(→I)	(discharges 2)
4	From (2) and (3), conclude b → (b → a)	(→I)	(discharges 2)

• No, because assumption 1 is still undischarged

• So the proof is incomplete

• (Discharging assumption 2 twice is actually OK)

• What if we did this instead:

1	Assume a
2	Assume b
3	From (2) and (1), conclude b → a	(→I)	(discharges 2)
4	From (2) and (3), conclude b → (b → a)	(→I)	(discharges 2)
5	From (1) and (4), conclude a → (b → (b → a))	(→I)	(discharges 1)

• Yeah, that's okay.

• By the way, a -> (b -> (b -> a)) is inhabited:

         foo a = \b -> (\b -> a)          :: a -> (b -> (b -> a))