∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} (motive : (x : List α) → (x_1 : List β) → (a, b) ∈ x.zip x_1 → Prop)
  (x : List α) (x_1 : List β) (x_2 : (a, b) ∈ x.zip x_1),
  (∀ (head : α) (l₁ : List α) (head_1 : β) (l₂ : List β) (h : (a, b) ∈ (head :: l₁).zip (head_1 :: l₂)),
      motive (head :: l₁) (head_1 :: l₂) h) →
    motive x x_1 x_2