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