case left | right =>
  split_ifs
  case pos c1 =>
    subst c1
    tauto
  case neg c1 =>
    rfl
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
no goals