contradiction
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h2 : M.t + 1 ≠ M.t + 1
h1 : v ∈ MultiPart.P M (M.t + 1)
⊢ v ∈ B
no goals