PLFA: Induction

Programming Language Foundations in Agda, Induction: Proof by Induction.

Temporarily public but I’ll make this private soon.

The exercises are extremely uneven. *-comm is really hard (or, counter-intuitive and confusing, since I always think suc n is just n + 1 and always assume tons of things), and others, including those “streches”, are easy to the extent that I didn’t have the patience to solve. Solved exercises:

1. +-swap, line 90;
2. *-distrib, line 103;
3. *-assoc, line 131;
4. *-comm, line 147;
5. 0∸n≡0, line 204.