simp [ih h]
case Lam
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
σ : 𝕋 𝕍
M : Λ V 𝕍
ih : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
Γ Γ' : TCtxt V 𝕍
h✝ : ∀ (x : V), x ∈ freeVarsOfTerm (λ' y : σ, M) → getType x Γ = getType x Γ'
h : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x (Γ;; y : σ) = getType x (Γ';; y : σ)
⊢ typeOf Γ (λ' y : σ, M) = typeOf Γ' (λ' y : σ, M)
no goals