toSubstitution

The single-binding Substitution this Equation amounts to, i.e. its Var side unified with the other side.

if neither lhs nor rhs is a Var (this Equation is not an Assignment).