split_ifs with h
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ some σ' = if y = x then some σ else some σ'
case pos.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ some σ' = some σ

case pos.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : ¬y = x
⊢ some σ' = some σ'