The unification problem is given the problem
statement t =? t', find a most general
substitution s such that s(t) = s(t') modulo
the axioms of a commutative monoid.
Substitition s is more general than s' if
there is a substitition s" such that s' =
s" o s.
