Most general unifier
= Most general unifier
= MGU
{c}
{synonym}
A most general unifier is a unifying substitution through which every other unifier factors by a further substitution. It records exactly the equality constraints forced by the terms.