cases c2
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
c2 : v = y ∧ y ∉ binders
a1 : t = x ∨ t = t
⊢ v ∉ binders
case intro
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : t = x ∨ t = t
left✝ : v = y
right✝ : y ∉ binders
⊢ v ∉ binders