∀ {α : Type u_3} {β : Type u_2} {γ : Type u_1} (motive : (α → γ → γ × β) → List α → γ → Prop) (x : α → γ → γ × β)
  (x_1 : List α) (x_2 : γ),
  (∀ (f : α → γ → γ × β) (head : α) (x : List α) (s : γ), motive f (head :: x) s) →
    (∀ (x : α → γ → γ × β) (x_3 : γ), motive x [] x_3) → motive x x_1 x_2