case eq_ x y =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    intro a1
    split_ifs at a1
    case _ c1 c2 =>
      cases c1
      case intro c1_left c1_right =>
        subst c1_left
        exact c1_right
    case _ c1 c2 =>
      cases c1
      case intro c1_left c1_right =>
        subst c1_left
        exact c1_right
    case _ c1 c2 =>
      cases c2
      case intro c2_left c2_right =>
        subst c2_left
        exact c2_right
    case _ c1 c2 =>
      tauto
v t x y : VarName
binders : Finset VarName
h1 : ¬(t = x ∨ t = y)
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
no goals