Proof.Language

• Types
• Terms
• Size of types and terms
• Substituion
• Free variables
• Context
• Opening

Proof.Subtyping.Splitable

• Definitions
• Splitable and Ordinary
• Automations
• Splitable or Ordinary
• Determinism of Splitable
• Unify Splitable Varialbes
• Decidablility of Ordinary
• Splitable & Size

Proof.Subtyping.Subtyping

• Definition
• Generlization
• Reflexivity
• Subtyping & Splitable
• Inversion Lemmas
• Proper Types
  • Definition
  • Completeness
  • Proper Induction Principle
• Transitivity
• Isomorphic Subtyping
  • Definition
  • Transitivity
  • Specficiation
• Subtyping & Isomorphic Subtyping
• Automations
  • Absurd Cases

Proof.Appsub

• Definitions
  • Arguments
  • Applicative Subtyping (Binary)
  • Applicative Subtyping
• Automations
  • Structural Inversions
  • Contradictions
• Properties
  • Determinism
• Appsub & Isomorphic Subtyping
  • Inversion Lemmas
  • Arguments
  • Functions
  • Generalization
• Function Definition
  • Soundness
  • Completeness
  • Automations

Proof.Value

• Definitions
  • Locally Closed
  • Partial Value
  • Universal Value
  • Value
• Automations
  • Solve LC
  • Structural Inversion
  • Contradictions
  • Solve Value
• Properties
  • Decidability

Proof.PrincipalTyping

• Definition
• Properties
  • Determinism

Proof.Typing

• Definition
• Typing & PrincipalTyping
• Typing & LC
• Check Subsumption

Proof.Casting

• Definition
• Casting & Value
• Progress
• Preservation

Proof.Application

• Definition
• Determinism
• App & Value
• Weakening Lemma
• Subsitution Lemma
• Preservation
• Progress

Proof.Reduction

• Definition
• Value
• Preservation
• Progress
• Soundness

Proof.LocallyNameless

Proof.Tactical

• introv
• gen
• exploit