rw [Order.lex_impl]
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝² property✝¹ property✝ : List.length [] = m
h : Order.lex_impl { val := [], property := property✝² } { val := [], property := property✝¹ }
⊢ Order.lex_impl (Variables.mul { val := [], property := property✝² } { val := [], property := property✝ })
    (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ })
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
property✝² property✝¹ property✝ : List.length [] = m
h : Order.lex_impl { val := [], property := property✝² } { val := [], property := property✝¹ }
⊢ match Variables.mul { val := [], property := property✝² } { val := [], property := property✝ },
    Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ } 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 (Variables.mul { val := [], property := property✝² } { val := [], property := property✝ }))
        (Vector.tail (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ }))
    else x ≤ y