Formalize the cumulative hierarchy V (most of §10.5 of the book)

This is joint work with Bas Spitters.
It formalizes exercise 10.11 (the "pushout" definition of V), where we had to slightly modify the induction principle given in the book in order to make it provable (see V_rect').
Then most of section 10.5 is proven (up to theorem 10.5.8).
This doesn't break CoqIde (that's what I use), but I agree it is kind of unconventional. I tried using "refine (let bisim_aux : its_type := _ in _).", but it makes the second part of the proof less readable, and I think it slows down the compilation a few seconds. Any other idea ?