{α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive 0 x) →
          ((n : ℕ) → motive n.succ []) → ((n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)) → motive x x_1