simp
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ (if y = x then some σ else getType y Γ) = typeOf Γ (if x = y then N else Λ.Var y)