{V : Type u} →
  {G : SimpleGraph V} →
    {v : V} →
      {motive : {w : V} → (a : G.Walk v w) → a.Nil → Sort u_1} →
        motive SimpleGraph.Walk.nil ⋯ → {w : V} → {a : G.Walk v w} → (t : a.Nil) → motive a t