case intro c1_left c1_right =>
  subst c1_left
  exact c1_right
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
no goals