intro h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ v ≠ v → ¬v ∈ A
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
h : v ≠ v
⊢ ¬v ∈ A