∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (x v_1 : V) (r : G.Adj v v_1) (p : G.Walk v_1 w)
  (x_1 : x ∈ (SimpleGraph.Walk.cons r p).support),
  (SimpleGraph.Walk.cons r p).takeUntil x x_1 =
    if hx : v = x then hx ▸ SimpleGraph.Walk.nil else SimpleGraph.Walk.cons r (p.takeUntil x ⋯)