∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} {v_1 : V} {h_1 : G.Adj u v_1}
  {p_1 : G.Walk v_1 w}, SimpleGraph.Walk.cons h p = SimpleGraph.Walk.cons h_1 p_1 → v = v_1 ∧ p ≍ p_1