∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  (funType_1 : (x : List (List α)) → (x_1 : List (List β)) → List.Forall₂ (List.Forall₂ R) x x_1 → Prop)
  (motive :
    (x : List (List α)) →
      (x_1 : List (List β)) → (x_2 : List.Forall₂ (List.Forall₂ R) x x_1) → List.Forall₂.below x_2 → Prop)
  (x : List (List α)) (x_1 : List (List β)) (x_2 : List.Forall₂ (List.Forall₂ R) x x_1)
  (below : List.Forall₂.below x_2),
  (∀ (a : Unit), motive [] [] ⋯ ⋯) →
    (∀ (a : List α) (b : List β) (l₁ : List (List α)) (l₂ : List (List β)) (h₁ : List.Forall₂ R a b)
        (h₂ : List.Forall₂ (List.Forall₂ R) l₁ l₂) (ih : List.Forall₂.below h₂) (a_ih : funType_1 l₁ l₂ h₂),
        motive (a :: l₁) (b :: l₂) ⋯ ⋯) →
      motive x x_1 x_2 below