∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V},
  (∀ (p : G.Walk v w), s(v, w) ∈ p.edges) →
    ∀ (c : G.Walk u u), c.IsTrail → ∀ (he : s(v, w) ∈ c.edges), w ∈ (c.takeUntil v ⋯).support → False