case eq_ x y =>
  simp
  constructor
  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
⊢ BoolFormula.eq_ (decide (x ∈ binders)) (decide (y ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = x then u else x) ∈ binders)) (decide ((if v = y then u else y) ∈ binders))
no goals