Next: Induction Principle
Up: classnote 14
Previous: Surface Syntax
We inherit several properties from the data typing of 
-terms:
- induction principle
- equality definition
- recursive definition using
In Fall 93, establishing those properties required work.