split_ifs <;> tauto
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
no goals