∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (v v_1 : V)
  (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h p) 0)
  (h_3 : (v v_2 : V) → (h : G.Adj u v_2) → (q : G.Walk v_2 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (match v, SimpleGraph.Walk.cons h p, 0 with
    | .(u), SimpleGraph.Walk.nil, x => h_1 x
    | v, SimpleGraph.Walk.cons h p, 0 => h_2 v v_2 h p
    | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_2 h q n) =
    h_2 v v_1 h p