split_ifs
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ y ∈ binders ↔ (if v = y then u else y) ∈ binders
case pos
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
h✝ : v = y
⊢ y ∈ binders ↔ u ∈ binders

case neg
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
h✝ : ¬v = y
⊢ y ∈ binders ↔ y ∈ binders