{α : Type u_1} →
  (motive : List α → List (List α) → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : List (List α)) →
        (x_2 : Array α) →
          ((x : List α) → (acc : Array α) → motive x [] acc) →
            ((x y : List α) → (xs : List (List α)) → (acc : Array α) → motive x (y :: xs) acc) → motive x x_1 x_2