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