rw [Order.lex_impl]
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝ : List.length (x :: xs) = m
⊢ Order.lex_impl { val := x :: xs, property := property✝ } { val := x :: xs, property := property✝ }
n : ℕ
a : Variables n order.Lex
m : ℕ
v : Variables m order.Lex
x : ℕ
xs : List ℕ
property✝ : List.length (x :: xs) = m
⊢ match { val := x :: xs, property := property✝ }, { val := x :: xs, property := property✝ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x_1 :: tail, property := property }, { val := y :: tail_1, property := property_1 } =>
    if x_1 = y then
      Order.lex_impl (Vector.tail { val := x :: xs, property := property✝ })
        (Vector.tail { val := x :: xs, property := property✝ })
    else x_1 ≤ y