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