∀ {α : Type u_1} {β : Type u_2} (as : List α)
  (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) (acc : Array β)
  (h : [].length + acc.size = as.length)
  (h_1 : (acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h)
  (h_2 :
    (a : α) →
      (as_1 : List α) → (acc : Array β) → (h : (a :: as_1).length + acc.size = as.length) → motive (a :: as_1) acc h),
  (match [], acc, h with
    | [], acc, h => h_1 acc h
    | a :: as_1, acc, h => h_2 a as_1 acc h) =
    h_1 acc h