∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop) (x : List α) (x_1 : List β),
  (∀ (acc : List β), motive [] acc) → (∀ (a : α) (l : List α) (acc : List β), motive (a :: l) acc) → motive x x_1