simp [Order.grlex.elem_sum, Variables.mul]
n : ℕ
a b : Variables n order.GrLex
property✝¹ property✝ : List.length [] = n
⊢ Order.grlex.elem_sum (Variables.mul { val := [], property := property✝¹ } { val := [], property := property✝ }) =
    Order.grlex.elem_sum { val := [], property := property✝¹ } +
      Order.grlex.elem_sum { val := [], property := property✝ }
no goals