Merge pull request #446 from JasonGross/no-match-pair

Don't match on pairs where we don't need to
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.
Allow [binder apply] to take a side-condition tac

Also, add an example with explanation.
Add a shorter more basic [binder apply] example

Also add [test] and [not] tacticals to [Overture.v].  For explanatory
purposes, there's now a [binder apply lem], not just [binder apply lem
in H].
Merge pull request #444 from JasonGross/binder-apply

Apply under binders
Merge pull request #448 from mikeshulman/rsu

improve some proofs and names in ReflectiveSubuniverse.v
Merge pull request #440 from jledent/master

Formalize the cumulative hierarchy V (most of §10.5 of the book)
unify ap_ap10 and apD10_ap_*