case eq_ x y =>
  simp at h2
  cases h2
  case intro h2_left h2_right =>
    intros a1
    cases a1
    case inl a1 =>
      subst a1
      simp at h2_left
      tauto
    case inr a1 =>
      subst a1
      simp at h2_right
      tauto
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  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))
⊢ v = x ∨ v = y → u ∉ binders
no goals