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