Fix unidirectional unification.

The unidirectional unifier now works on examples such as a+b*c =>
d+e*f. This required a couple of changes to the algorithm, the main
one being that we allow variables to match against subtrees of the
expression.