by_contra h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
⊢ v ∈ M.A
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
h : ¬v ∈ M.A
⊢ False