∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop) (as : List α) (bs : List β),
  (∀ (x : List β), motive [] x) →
    (∀ (x : List α), motive x []) →
      (∀ (a : α) (as : List α) (b : β) (bs : List β), motive (a :: as) (b :: bs)) → motive as bs