- Matching Integer Comparisons
- Some Properties of Well-foundation
- Useful Properties of Basic Datatypes
- Definition of Syntax
- Definition of Subclassing
- Definition of Substitutions
- Definitions about De Bruijn's Indices
- Definition of Type Ordering
- Definition of Path Typing, Subtyping, Term Typing
- Definition of Semantics
- Miscellaneous properties
- Proofs about Type Ordering
- Proofs about Subclassing
- Proofs about Admissibility of Transitivity for Subtyping
- Proof of the Progress Property
- Proofs about De Bruijn's Indices
- Proofs about Substitution for the Current Instance
- Proofs about Substitution for Parameters
- Proofs about Substitution for a Local Variable
- Proof of the Subject Reduction Property
- Proof of Type Safety

This page has been generated by coqdoc