Proof of the boundary transition lemma

Scan the left side of a cut, introducing each vertex's right neighbors before forgetting it. Charge every bag vertex except the vertex being forgotten to a distinct crossing edge. This is the middle decomposition in Fomin and Høie's proof of their cubic-graph pathwidth theorem (Theorem 5, 2006).

theorem Algebraic.Cutwidth.PathDecomposition.Internal.exists_boundaryTransition {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (left : ∀ u ∈ S, ∃ v ∉ S, H.Adj u v) (right : ∀ v ∉ S, ∃ u ∈ S, H.Adj u v) : ∃ (D : PathDecomposition H) (first : Fin D.length) (last : Fin D.length), (∀ (i : Fin D.length), first ≤ i ∧ i ≤ last) ∧ D.bag first = S ∧ D.bag last = Sᶜ ∧ ∀ (i : Fin D.length), (D.bag i).card ≤ (H.cutFinset S).card + 1