∀ {V : Type u} {G : SimpleGraph V} {v u : V} [inst : DecidableEq V] {w x : V} (p : G.Walk u v) (hw : w ∈ p.support)
  (hx : x ∈ (p.takeUntil w hw).support), (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯