And the solution is essentially to delegate not both alpha equivalents and substitution, but only alpha equivalence to the meta-language. And therefore tae a non-structured class of object variables called names and define that in your set but here the negative occurrence is replaced by an occurrence of this new unstructured set. So, we do not delegate substitution terms for names, but only names for names.

---