left
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : ¬a = v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : ¬a = v
⊢ a ∈ A ∧ ¬a ∈ B