congr! 1
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ eq_ (σ x) (σ y) = eq_ (σ' x) (σ' y)
case h.e'_1
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ x = σ' x

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