inductive typing : context → Trm → Typ → Prop

• typ_var (Γ : context) (x : ℕ) (T : Typ) : valid_ctx Γ → binds x T Γ → typing Γ ($x) T
• typ_abs (L : Finset ℕ) (Γ : context) (t : Trm) (T1 T2 : Typ) : (∀ x ∉ L, typing ((x, T1) :: Γ) (t.open₀ ($x)) T2) → typing Γ (λ T1,t) (T1 -> T2)
• typ_app (Γ : context) (t₁ t₂ : Trm) (T1 T2 : Typ) : typing Γ t₁ (T1 -> T2) → typing Γ t₂ T1 → typing Γ (t₁ @ t₂) T2

theorem typing_valid_ctx (Γ : context) (t : Trm) (T : Typ) : typing Γ t T → valid_ctx Γ

theorem typing_weakening_strengthened' (Γ Δ Ψ' : context) (t : Trm) (T : Typ) : typing Ψ' t T → ∀ (Ψ : context), Ψ' = Ψ ++ Γ → valid_ctx (Ψ ++ Δ ++ Γ) → typing (Ψ ++ Δ ++ Γ) t T

theorem typing_weakening_strengthened (Γ Δ Ψ : context) (t : Trm) (T : Typ) : typing (Ψ ++ Γ) t T → valid_ctx (Ψ ++ Δ ++ Γ) → typing (Ψ ++ Δ ++ Γ) t T

theorem typing_weakening (Γ Δ : context) (t : Trm) (T : Typ) : typing Γ t T → valid_ctx (Δ ++ Γ) → typing (Δ ++ Γ) t T

theorem typing_weakening_head (Γ : context) (t : Trm) (T S : Typ) (x : ℕ) : ¬in_context x Γ → typing Γ t T → typing ((x, S) :: Γ) t T

theorem typing_subst_var_case (Γ Δ : context) (u : Trm) (S T : Typ) (z x : ℕ) : binds x T (Δ ++ (z, S) :: Γ) → valid_ctx (Δ ++ (z, S) :: Γ) → typing Γ u S → typing (Δ ++ Γ) ([z // u] $x) T

theorem typing_regular (t : Trm) (T : Typ) (Γ : context) : typing Γ t T → t.lc

theorem typing_subst_strengthened' (Γ Δ' : context) (t u : Trm) (S T : Typ) (z : ℕ) : typing Δ' t T → ∀ (φ : context), Δ' = φ ++ (z, S) :: Γ → typing (φ ++ (z, S) :: Γ) t T → typing Γ u S → typing (φ ++ Γ) ([z // u] t) T

theorem typing_subst_strengthened (Γ Δ : context) (t u : Trm) (S T : Typ) (z : ℕ) : typing (Δ ++ (z, S) :: Γ) t T → typing Γ u S → typing (Δ ++ Γ) ([z // u] t) T

theorem typing_subst (Γ : context) (t u : Trm) (S T : Typ) (z : ℕ) : typing ((z, S) :: Γ) t T → typing Γ u S → typing Γ ([z // u] t) T

theorem typing_rename (Γ : context) (x y : ℕ) (t : Trm) (T1 T2 : Typ) : x ∉ t.fv → ¬in_context x Γ → y ∉ t.fv → ¬in_context y Γ → typing ((x, T1) :: Γ) (t.open₀ ($x)) T2 → typing ((y, T1) :: Γ) (t.open₀ ($y)) T2

theorem typing_abs_intro (Γ : context) (x : ℕ) (t : Trm) (T1 T2 : Typ) : x ∉ t.fv → ¬in_context x Γ → typing ((x, T1) :: Γ) (t.open₀ ($x)) T2 → typing Γ (λ T1,t) (T1 -> T2)

theorem preservation_beta_red (E : context) (t : Trm) (T : Typ) : typing E t T → ∀ (t' : Trm), beta_red t t' → typing E t' T

theorem preservation_multi_red (E : context) (t : Trm) (T : Typ) : typing E t T → ∀ (t' : Trm), multi_red t t' → typing E t' T