∀ {α : Type u_1} (cmp : α → α → Ordering) (x_2 : α) (xs : List α) (y : α) (ys : List α),
  List.compareLex cmp (x_2 :: xs) (y :: ys) =
    match cmp x_2 y with
    | Ordering.lt => Ordering.lt
    | Ordering.eq => List.compareLex cmp xs ys
    | Ordering.gt => Ordering.gt