rw [Order.lex_impl]
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
h : Order.lex_impl { val := x :: xs, property := p₁ } { val := y :: ys, property := p₂ }
⊢ Order.lex_impl (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ })
    (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ })
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
m : ℕ
a b c : Variables m order.Lex
x : ℕ
xs : List ℕ
p₁ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
p₂ : List.length (y :: ys) = m
z : ℕ
zs : List ℕ
p₃ : List.length (z :: zs) = m
h : Order.lex_impl { val := x :: xs, property := p₁ } { val := y :: ys, property := p₂ }
⊢ match Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ },
    Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ } with
  | { val := [], property := property }, { val := [], property := property_1 } => True
  | { val := x_1 :: tail, property := property }, { val := y_1 :: tail_1, property := property_1 } =>
    if x_1 = y_1 then
      Order.lex_impl (Vector.tail (Variables.mul { val := x :: xs, property := p₁ } { val := z :: zs, property := p₃ }))
        (Vector.tail (Variables.mul { val := y :: ys, property := p₂ } { val := z :: zs, property := p₃ }))
    else x_1 ≤ y_1