∀ {α : Type u_1} {r : α → α → Prop} (motive : (as bs : List α) → ¬List.Lex r bs as → ¬List.Lex r as bs → Prop)
  (as bs : List α) (h₁ : ¬List.Lex r bs as) (h₂ : ¬List.Lex r as bs),
  (∀ (h₁ h₂ : ¬List.Lex r [] []), motive [] [] h₁ h₂) →
    (∀ (head : α) (tail : List α) (h₁ : ¬List.Lex r (head :: tail) []) (h₂ : ¬List.Lex r [] (head :: tail)),
        motive [] (head :: tail) h₁ h₂) →
      (∀ (head : α) (tail : List α) (h₁ : ¬List.Lex r [] (head :: tail)) (h₂ : ¬List.Lex r (head :: tail) []),
          motive (head :: tail) [] h₁ h₂) →
        (∀ (a : α) (as : List α) (b : α) (bs : List α) (h₁ : ¬List.Lex r (b :: bs) (a :: as))
            (h₂ : ¬List.Lex r (a :: as) (b :: bs)), motive (a :: as) (b :: bs) h₁ h₂) →
          motive as bs h₁ h₂