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

Don't match on pairs where we don't need to
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].