Now, it is remarkable that with these simple axioms we did derive the meta-theory of all these object calculi, thus proving that a higher order constructive type theory which uses higher order abstract syntax together with a suitable collection of axioms can be a very successful metamodel.

---