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