subst c1_left
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
v t y : VarName
binders : Finset VarName
c2 : v = y ∧ y ∉ binders
a1 : t = t ∨ t = t
h1 : t ≠ v ∧ t ≠ y
c1_right : v ∉ binders
⊢ v ∉ binders