Allow [binder apply] to take a side-condition tac

Also, add an example with explanation.
WIP