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