Add 'unify' tactic

Normally, we give every explicit argument to a function after 'refine',
even if some may be solvable by unification. The 'unify' tactic goes
back and fills in the unifiable ones.

(I don't expect this to be useful *that* often but I have occasionally
encountered such situations.)