subst c2_left
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
c2_left : v = y
c2_right : y ∉ binders
⊢ v ∉ binders
v t x : VarName
binders : Finset VarName
h1_left : t ≠ x
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
h1_right : t ≠ v
c2_right : v ∉ binders
⊢ v ∉ binders