∀ {V : Type u_1} {G : SimpleGraph V} {u v v' : V} {p : G.Walk u v} (i : ℕ),
  (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length →
    i + 1 ≤ p.length