List.Lex.to_ne

theorem List.Lex.to_ne : ∀ {α : Type u} {l₁ l₂ : List α}, List.Lex (fun x x_1 => x ≠ x_1) l₁ l₂ → l₁ ≠ l₂

This theorem states that for any type `α` and any two lists `l₁` and `l₂` of this type, if there exists a lexicographical order (denoted by `List.Lex`) between `l₁` and `l₂` such that no two elements `x` and `x_1` are equal (denoted by `x ≠ x_1`), then `l₁` is not equal to `l₂`. In other words, if two lists are different in a lexicographical order which does not allow equal elements, then the lists themselves are not equal.

More concisely: If `α` is a type and `l₁` and `l₂` are two lists of type `α` such that `l₁` is lexicographically smaller than `l₂` and no element in `l₁` is equal to any element in `l₂`, then `l₁ ≠ l₂`.