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].