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