The induction principle for -terms is obtained from the induction principle for recursively defined types:
The hypothesis uses cases on :
-terms is obtained from the
induction principle for recursively defined types:
:
