intro hv hw
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
⊢ v ∈ C → w ∈ C → ¬Adj (mp (minsert M h)) v w
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
⊢ ¬Adj (mp (minsert M h)) v w