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