match a, b with
  | ⟨[], _⟩   , ⟨[], _⟩    => simp [Order.grlex.elem_sum, Variables.mul]
  | ⟨x::xs, p⟩, ⟨y::ys, q⟩ => simp [Order.grlex.elem_sum, Variables.mul]
                              simp [List.zipWith]
                              simp [foldl_cons]
                              have size_eq : (x::xs).length = (y::ys).length
                              rw [Eq.symm q] at p
                              exact p
                              have tails_size_eq : xs.length = ys.length
                              simp at size_eq
                              exact size_eq
                              have hh := zipWith_to_fold x y xs ys tails_size_eq
                              simp [algebra.sum] at hh 
                              simp [hh]
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex.elem_sum (Variables.mul a b) = Order.grlex.elem_sum a + Order.grlex.elem_sum b
no goals