∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x : α × β}
  (motive : (y : α × β) → (G □ H).Walk x y → Sort u_3) (y v : α × β) (h : (G □ H).Adj x v) (w : (G □ H).Walk v y)
  (h_1 : Unit → motive x SimpleGraph.Walk.nil)
  (h_2 : (y v : α × β) → (h : (G □ H).Adj x v) → (w : (G □ H).Walk v y) → motive y (SimpleGraph.Walk.cons h w)),
  (match y, SimpleGraph.Walk.cons h w with
    | .(x), SimpleGraph.Walk.nil => h_1 ()
    | y, SimpleGraph.Walk.cons h w => h_2 y v h w) =
    h_2 y v h w