case intro c2_left c2_right =>
  subst c2_left
  exact c2_right
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : t = x ∨ t = t
c2_left : v = y
c2_right : y ∉ binders
⊢ v ∉ binders
no goals