intro Γ Γ' h
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ') →
      typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)
case App
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
⊢ typeOf Γ (Λ.App M N) = typeOf Γ' (Λ.App M N)