simp [h', h'']
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : ¬z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
no goals