Weird inductive types

This is an attempt at finally closing #615.  Some remarks:

* I tried to explain both possible recursors in section 5.6, but I'm open to suggestions for improvement.  Because #601 is still stalled, I wasn't able to give a number to the second one, making backreferences from the exercises kind of clumsy.

* I took the liberty of inserting two new exercises in between ex. 5.8 and Marc's new ex 5.9, renumbering the latter to 5.11.  Since the latter was only merged this morning and hasn't been posted yet, I didn't feel bad about this.  Even better would be for the two new exercises to come in between ex. 5.7 and ex. 5.8, but again we can't do this unless #601 is resolved.

* In ex. 5.8, I tried to give a recursor that includes the predecessor as well, matching the book's terminology elsewhere (omitting the predecessor is referred to as the "iterator" in ex. 1.4), along with a computation rule.  However, I'd appreciate it if someone would check that I did it correctly.