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