intro h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
⊢ Adj (mp M) v w → i ≠ j
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : Adj (mp M) v w
⊢ i ≠ j