introv
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
⊢ ∀ (x : V), getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')