Systems of formal logic generally have inference rules that require certain expressions to be syntactically the same in multiple steps. Typically two steps are involved, as for modus ponens, where the rule works with two steps of the form "A" and "A => B", where A and B are arbitrary boolean terms. Such systems also generally allow substitution for free variables of a proved statement.
Unification algorithms are described as finding a single substitution which can then be applied to both of the (let's say two) proved statements to make appropriate parts the same after the substitution. Careful presentations though require the two sets of free variables of the two proved statements be made to have no names in common, a process sometimes referred to as "uniqueification".
In this case the resulting substitution can be split into two disjoint parts, one with the substituted variables from the first statement and the other one with the substituted variables from the second statement, since substituting for a variable that is not present in a term has no effect.
So: Are there practical algorithms that work directly on the given input terms without requiring the "uniqueification" step? In my case it is desirable to keep the original variable names for presentation purposes. It is also natural to present the result of the matching as multiple substitutions, one into each of the statements being matched. Hopefully such a unification algorithm would directly yield two substitutions.
I am presuming that two substitutions are always enough for rules that work on two input statements, but conceivably this is mistaken.