intro Γ Γ' h
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ ∀ {Γ Γ' : TCtxt V 𝕍},
    (∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ') →
      typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
Γ Γ' : TCtxt V 𝕍
h : ∀ (x_1 : V), x_1 ∈ freeVarsOfTerm (Λ.Var x) → getType x_1 Γ = getType x_1 Γ'
⊢ typeOf Γ (Λ.Var x) = typeOf Γ' (Λ.Var x)