∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [PartialEquivBEq α] (lt : α → α → Bool),
  (∀ (x y : α), (x == y) = true → lt x y = false) →
    (∀ (x y : α), lt x y = true → lt y x = false) →
      (∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true) →
        (l₁.lex l₂ lt = false ↔
          (l₂.isEqv (List.take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
            ∃ i,
              ∃ (h₁ : i < l₁.length) (h₂ : i < l₂.length),
                (∀ (j : ℕ) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true)