apply h1
case h.e'_2
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ y = σ' y
case h.e'_2.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = x ∨ y = y