There are also other interesting bits to this fact, the fact the we are using a l-calculus as a higher, as a meta-logical, as a metamodel, arises to deal in uniform and abstract way with binders.
And how does this work? Well, a meta-language variable of type A can be made to represent a generic object of type A
Hence a meta-language object of types A can play the role of a context of this type over objects of that type. This leads the way to the so called Higher Order Abstract Syntax paradigm and the higher order natural deduction paradigm.
The Higher Order Abstract Syntax paradigm is what I have what I have briefly introduced also in the previous lecture a generalisation of the algebra at first order way of specifying syntax.
In this way we can specify syntax with binders. And the basic idea is that we delegate to the meta-language that is l meta-language to this higher order l-calculus, which is in the background is our metamodel, all the machinery that has to deal with binding operators.