cases c1
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : v = x ∧ x ∉ binders
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders
case intro
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 = y) ∧ t ∉ binders
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders