Merge pull request #445 from marcbezem/master

Solution to Exercise 3.1 and two preparing lemmas added.
Move some [Require]s to the top of a file

It's bad practice to have them in the middle of the file.  Also, it
makes my coq-bug-finder run afoul of
https://coq.inria.fr/bugs/show_bug.cgi?id=3556 when tracking down a bug
in [apply] in the new version of trunk with #440.
Strip out a duplicate [Require Import]
Don't match on pairs where we don't need to

It's slightly better style, I think, to do it this way.  Also, when we
move to primitive projections, this code will break (see
https://coq.inria.fr/bugs/show_bug.cgi?id=3558).
Merge pull request #446 from JasonGross/no-match-pair

Don't match on pairs where we don't need to
Formalize the cumulative hierarchy V (most of §10.5 of the book)
Change the style of the comments
Move the dependent composition to Overture.v
Rename "bitot" as "bitotal"
Move is_mono_isinj to minus1Trunc.v
Add the Irreflexive & Asymmetric type classes to Overture.v
Make use of [transparent assert] in the proof of bisimulation.
Make use of curly braces, adjust indentation.
Split the proof of bisimulation again (this is much faster).
Forgot to update a file
Make V_comt_setext vacuous, change comment style
Apply under binders

This tactic will be useful for writing a rewrite modulo associativity
tactic.
remove unicode in ReflectiveSubuniverse.v
rename subuniverse predicate more descriptively
O_modal_equiv -> O_modal_isequiv