∀ {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).dropUntil x x_1 =
    if hx : v = x then
      Eq.ndrec (motive := fun u => u ∈ (SimpleGraph.Walk.cons r p).support → G.Walk u w)
        (fun h => SimpleGraph.Walk.cons r p) hx x_1
    else p.dropUntil x ⋯