∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : ℕ → List α → (List α → β) → (β → γ) → List β → List γ → Prop)
  (x : ℕ) (x_1 : List α) (x_2 : List α → β) (x_3 : β → γ) (x_4 : List β) (x_5 : List γ),
  (∀ (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ), motive 0 l f g r s) →
    (∀ (n : ℕ) (x : List α → β) (x_6 : β → γ) (x_7 : List β) (x_8 : List γ), motive n.succ [] x x_6 x_7 x_8) →
      (∀ (n : ℕ) (a : α) (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ),
          motive n.succ (a :: l) f g r s) →
        motive x x_1 x_2 x_3 x_4 x_5