⁵When unification is used at the metalevel (see Section 17.6.8), there are two possibilities: (i) a counter for new fresh variables must take into account the numbers used in the variables of the unification problem, or (ii) an identifier among ’#, ’%, and ’@ used in the variables of the unification problem.