∀ {α : Type u_1} (r : α → α → Prop) (funType_1 : (x x_1 : List α) → List.Lex r x x_1 → List.Lex r x_1 x → Prop)
  (motive :
    (x x_1 : List α) →
      (x_2 : List.Lex r x x_1) →
        List.Lex.below (motive := fun x x_3 x_4 => ∀ (x_5 : List.Lex r x_3 x), funType_1 x x_3 x_4 x_5) x_2 →
          List.Lex r x_1 x → Prop)
  (x x_1 : List α) (x_2 : List.Lex r x x_1)
  (below : List.Lex.below (motive := fun x x_3 x_4 => ∀ (x_5 : List.Lex r x_3 x), funType_1 x x_3 x_4 x_5) x_2)
  (x_3 : List.Lex r x_1 x),
  (∀ (a₁ : α) (l₁ : List α) (a₂ : α) (l₂ : List α) (h₁ : r a₁ a₂) (h₂ : r a₂ a₁), motive (a₁ :: l₁) (a₂ :: l₂) ⋯ ⋯ ⋯) →
    (∀ (a₁ : α) (l₁ l₂ : List α) (h₁ : r a₁ a₁) (h : List.Lex r l₂ l₁), motive (a₁ :: l₁) (a₁ :: l₂) ⋯ ⋯ ⋯) →
      (∀ (a : α) (l₁ l₂ : List α) (h : List.Lex r l₁ l₂) (h₂ : r a a)
          (ih : List.Lex.below (motive := fun x x_4 x_5 => ∀ (x_6 : List.Lex r x_4 x), funType_1 x x_4 x_5 x_6) h)
          (h_ih : ∀ (x : List.Lex r l₂ l₁), funType_1 l₁ l₂ h x), motive (a :: l₁) (a :: l₂) ⋯ ⋯ ⋯) →
        (∀ (a : α) (l₁ l₂ : List α) (h₁ : List.Lex r l₁ l₂) (h₂ : List.Lex r l₂ l₁)
            (ih : List.Lex.below (motive := fun x x_4 x_5 => ∀ (x_6 : List.Lex r x_4 x), funType_1 x x_4 x_5 x_6) h₁)
            (h_ih : ∀ (x : List.Lex r l₂ l₁), funType_1 l₁ l₂ h₁ x), motive (a :: l₁) (a :: l₂) ⋯ ⋯ ⋯) →
          motive x x_1 x_2 below x_3