intro v hv
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
⊢ ∀ (v : α), v ∈ B → v ∈ MultiPart.P (minsert M h) (M.t + 1)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1)