Capture avoiding substitution is a little problematic however if we take this sort of definition. I mean it is not problematic in this context because can do simply replacement. But, of course, when we will come to reasoning on this, and we will have to define inductively the set of terms, then we might encounter some problems. So, as I have said, within this metamodel we can directly encode higher order abstract syntax.

---