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