rw [Order.lex_impl]
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
⊢ Order.lex_impl { val := [], property := p } { val := [], property := l }
n : ℕ
v₁ v₂ v₃ : Variables n order.Lex
h₁ : Order.lex v₁ v₂
h₂ : Order.lex v₂ v₃
m : ℕ
a b c : Variables m order.Lex
p q l : List.length [] = m
ab : Order.lex_impl { val := [], property := p } { val := [], property := q }
bc : Order.lex_impl { val := [], property := q } { val := [], property := l }
⊢ match { val := [], property := p }, { val := [], property := l } 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 := l })
    else x ≤ y