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 Γ (λ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) (e : Trm) (T : Typ) : typing Γ e T → valid_ctx Γ

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

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

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

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

theorem typing_subst_var_case (Γ : context) (Δ : context) (u : Trm) (S : Typ) (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) (Δ' : context) (t : Trm) (u : Trm) (S : Typ) (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) (Δ : context) (t : Trm) (u : Trm) (S : Typ) (T : Typ) (z : ℕ) : typing (Δ ++ (z, S) :: Γ) t T → typing Γ u S → typing (Δ ++ Γ) ([z // u] t) T

theorem typing_subst (Γ : context) (t : Trm) (u : Trm) (S : Typ) (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 : Typ) (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 : Typ) (T2 : Typ) : x ∉ t.fv → ¬in_context x Γ → typing ((x, T1) :: Γ) (t.open₀ ($x)) T2 → typing Γ (λt) (T1 -> T2)

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

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