by_cases h' : z = x
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

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