∀ {α : Type u_1} (motive : List α → α → List α → List (List α) → Sort u_2) (ag : α) (r : List α) (acc : List (List α))
  (h_1 : (a : α) → (as : List α) → (b : α) → (r : List α) → (acc : List (List α)) → motive (a :: as) b r acc)
  (h_2 : (ag : α) → (r : List α) → (acc : List (List α)) → motive [] ag r acc),
  (match [], ag, r, acc with
    | a :: as, b, r, acc => h_1 a as b r acc
    | [], ag, r, acc => h_2 ag r acc) =
    h_2 ag r acc