∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop},
  let funType_1 := fun x x_1 x_2 x_3 x_4 x_5 => List.Forall₂ P (List.map x x_3) (List.map x_1 x_4);
  ∀
    (motive :
      (x : α → γ) →
        (x_1 : β → δ) →
          Relator.LiftFun R P x x_1 →
            (x : List α) →
              (x_2 : List β) →
                (x_3 : List.Forall₂ R x x_2) →
                  List.Forall₂.below (motive := fun x x_4 x_5 =>
                      ∀ (x_6 : α → γ) (x_7 : β → δ) (x_8 : Relator.LiftFun R P x_6 x_7),
                        funType_1 x_6 x_7 x_8 x x_4 x_5)
                      x_3 →
                    Prop)
    (x : α → γ) (x_1 : β → δ) (x_2 : Relator.LiftFun R P x x_1) (x_3 : List α) (x_4 : List β)
    (x_5 : List.Forall₂ R x_3 x_4)
    (below :
      List.Forall₂.below (motive := fun x x_6 x_7 =>
        ∀ (x_8 : α → γ) (x_9 : β → δ) (x_10 : Relator.LiftFun R P x_8 x_9), funType_1 x_8 x_9 x_10 x x_6 x_7) x_5),
    (∀ (x : α → γ) (x_6 : β → δ) (x_7 : Relator.LiftFun R P x x_6), motive x x_6 x_7 [] [] ⋯ ⋯) →
      (∀ (x : α → γ) (x_6 : β → δ) (h : Relator.LiftFun R P x x_6) (head : α) (tail : List α) (head_1 : β)
          (tail_1 : List β) (h₁ : R head head_1) (h₂ : List.Forall₂ R tail tail_1)
          (ih :
            List.Forall₂.below (motive := fun x x_7 x_8 =>
              ∀ (x_9 : α → γ) (x_10 : β → δ) (x_11 : Relator.LiftFun R P x_9 x_10), funType_1 x_9 x_10 x_11 x x_7 x_8)
              h₂)
          (a_ih : ∀ (x : α → γ) (x_7 : β → δ) (x_8 : Relator.LiftFun R P x x_7), funType_1 x x_7 x_8 tail tail_1 h₂),
          motive x x_6 h (head :: tail) (head_1 :: tail_1) ⋯ ⋯) →
        motive x x_1 x_2 x_3 x_4 x_5 below