case _ c1 c2 =>
  cases c1
  case intro c1_left c1_right =>
    subst c1_left
    exact c1_right
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : v = x ∧ x ∉ binders
c2 : ¬(v = y ∧ y ∉ binders)
a1 : t = t ∨ t = y
⊢ v ∉ binders
no goals