{α : Type u_1} →
  (motive : List ℕ → List α → Sort u_2) →
    (x : List ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive [] x) → ((n : ℕ) → (ns : List ℕ) → (x : List α) → motive (n :: ns) x) → motive x x_1