More unifier fixes.

unify().

Fixes to unification records:
  - Properly merge rmap.
  - Don't store redundant equations.

Other fixes:
  - Fix an issue where existing urecs weren't properly being merged
    in map_commut_assoc().

Fix avoidable exponential blowup in unifier.

Change the code to do what the previous code tried to do, which is to
match free variables only after matching the more complex terms. This
avoids iterating over all possible subsets of the RHS.

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.