TPIL 3.7 labeled exercises

Stream: new members

[Eduardo Cavazos]

I've posted a few questions to stackoverflow around the proofs in exercise 3.7. It'd be nice to reference individual ones by exercise number, except that they aren't individually labeled.

In case the authors think it would be helpful, I've added a pull request which itemizes the proofs. So when discussing these a reader can say "I have a question about exercise 3.7.1.ii":

https://github.com/leanprover/theorem_proving_in_lean/blob/2d70939d2ced1b4f626b07d24b655e894fee0a22/propositions_and_proofs.rst

(Scroll to the very bottom to see how they're labeled.)

No worries if not accepted. Just a suggestion. :-)

[Jeremy Avigad]

@Eduardo Cavazos I am sorry that it took me so long to get to this. I did something slightly different: it looked better to number the identities in the preceding section, and I moved the "try me!" code block to the exercises. Thanks for your help, and for all the recent corrections.