∀ {β : Type u_2} {α : Type u_1} (motive : List α → β → List β → Sort u_3) (x : α) (xs : List α) (last : β)
  (acc : List β) (h_1 : (last : β) → (acc : List β) → motive [] last acc)
  (h_2 : (x : α) → (xs : List α) → (last : β) → (acc : List β) → motive (x :: xs) last acc),
  (match x :: xs, last, acc with
    | [], last, acc => h_1 last acc
    | x :: xs, last, acc => h_2 x xs last acc) =
    h_2 x xs last acc