simp [h]
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
x : V
σ τ : 𝕋 𝕍
aux : Option (𝕋 𝕍)
τ' : 𝕋 𝕍
h' : typeOf (Γ;; x : σ) M = some τ'
h : τ' = τ
⊢ some τ' = some τ
no goals