∀ {V : Type u_1} {G : SimpleGraph V} (H : SimpleGraph V)
  (motive : (u v : V) → (p : G.Walk u v) → (∀ e ∈ p.edges, e ∈ H.edgeSet) → Sort u_2) (u w v : V) (h : G.Adj u v)
  (p : G.Walk v w) (h_1 : ∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet)
  (h_1_1 : (u : V) → (h : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∈ H.edgeSet) → motive u u SimpleGraph.Walk.nil h)
  (h_2 :
    (u w v : V) →
      (h : G.Adj u v) →
        (p : G.Walk v w) →
          (h_2 : ∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet) →
            motive u w (SimpleGraph.Walk.cons h p) h_2),
  (match u, w, SimpleGraph.Walk.cons h p, h_1 with
    | u, .(u), SimpleGraph.Walk.nil, h => h_1_1 u h
    | u, w, SimpleGraph.Walk.cons h p, h_3 => h_2 u w v h p h_3) =
    h_2 u w v h p h_1