∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (w : ℕ),
  (∀ (i : ℕ) (h : i + 1 ≤ [u', v'].length), p.support[w + i]? = some [u', v'][i]) →
    1 ≤ [u', v'].length → w < p.support.length