{α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → Array β → Sort u_3) →
      (x : List α) →
        (x_1 : Array β) →
          ((acc : Array β) → motive [] acc) →
            ((a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc) → motive x x_1