So, schemata are represented as higher order objects and substitution instantiation is encoded by b-reduction. So, higher order abstract syntax sets a standard for a-conversion and for the mechanism of capture avoiding substitution. And of course also binders.