∀ {α : Type u_1} (motive : ℕ → List α → Prop) (x : ℕ) (x_1 : List α),
  (∀ (a : Unit), motive 0 []) →
    (∀ (head : α) (tail : List α), motive 0 (head :: tail)) →
      (∀ (n : ℕ), motive n.succ []) → (∀ (n : ℕ) (x : α) (xs : List α), motive n.succ (x :: xs)) → motive x x_1