∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.SublistForall₂ R a a_1 → Prop}
  {motive_1 : {a : List α} → {a_1 : List β} → (t : List.SublistForall₂ R a a_1) → List.SublistForall₂.below t → Prop},
  (∀ {l : List β}, motive_1 ⋯ ⋯) →
    (∀ {a₁ : α} {a₂ : β} {l₁ : List α} {l₂ : List β} (a : R a₁ a₂) (a_1 : List.SublistForall₂ R l₁ l₂)
        (ih : List.SublistForall₂.below a_1) (a_ih : motive l₁ l₂ a_1), motive_1 a_1 ih → motive_1 ⋯ ⋯) →
      (∀ {a : β} {l₁ : List α} {l₂ : List β} (a_1 : List.SublistForall₂ R l₁ l₂) (ih : List.SublistForall₂.below a_1)
          (a_ih : motive l₁ l₂ a_1), motive_1 a_1 ih → motive_1 ⋯ ⋯) →
        ∀ {a : List α} {a_1 : List β} {t : List.SublistForall₂ R a a_1} (t_1 : List.SublistForall₂.below t),
          motive_1 t t_1