A very important feature of this metamodel, this logical framework, is the way that it handles recursion and induction principles. This indeed is one of the major tools that we use in proofs and hands also one of the major tools that we use functional programming. Now, let me just briefly describe how the sort of relation that exists between induction principles and recursion principles. Look at the general type of a recursor. You can see that it has for all P, or for all propositions, if this is true of 0 and if it is true of n, then it is true of S of n and it holds for all of n. And well, this is essentially the induction principle. The only difference is that in induction principles you use predicates, that is functions going from natural numbers to propositions, while in this case you use functions going from natural numbers to sets over a data type.

---