∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Prop) (v : V) (x : G.Walk u v),
  (∀ (a : Unit), motive u SimpleGraph.Walk.nil) →
    (∀ (v v_1 : V) (h : G.Adj u v_1) (p : G.Walk v_1 v), motive v (SimpleGraph.Walk.cons h p)) → motive v x