congr! 1
σ σ' : VarName → VarName
x y : VarName
binders : Finset VarName
h1 : ∀ v ∉ binders, σ v = σ' v
⊢ eq_ (if x ∉ binders then σ x else x) (if y ∉ binders then σ y else y) =
    eq_ (if x ∉ binders then σ' x else x) (if y ∉ binders then σ' y else y)
case h.e'_1
σ σ' : VarName → VarName
x y : VarName
binders : Finset VarName
h1 : ∀ v ∉ binders, σ v = σ' v
⊢ (if x ∉ binders then σ x else x) = if x ∉ binders then σ' x else x

case h.e'_2
σ σ' : VarName → VarName
x y : VarName
binders : Finset VarName
h1 : ∀ v ∉ binders, σ v = σ' v
⊢ (if y ∉ binders then σ y else y) = if y ∉ binders then σ' y else y