LambdaProj.Infrastructure

• Partial Maps
• Custom Tactic

LambdaProj.Definitions

• Syntax
• Well-Formedness
• Substitution
• Reduction
• Normal Forms
• Subtyping
• Typing

LambdaProj.Proofs

• Well-Formedness
• Field Lookup
• Inversion Lemmas
• Progress
• Weakening Lemmas
• Preservation
• Type Soundness