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).
`Definition`s should not go inside proofs.  Ever.  `Let`s should probably also not go inside proofs.  If you want it to be proof-local, use `pose ($body) as $name` (`pose ($name := $body)` might also work).  If you want to build it line-by-line using tactics, here's a tactic we should maybe stick in `Overture.v`, taking advantage of dependent subgoals:

```coq
Tactic Notation "transparent" "assert" "(" ident(name) ":" open_constr(type) ")" :=
  refine (let H := (_ : type) in _);
  [
  | let H := match goal with H := _ |- _ => constr:(H) end in
    rename H into name ].
```