simp [algebra.sum] at hh
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
hh :
  foldl algebra.sum (x + y) (zipWith algebra.sum xs ys) = algebra.sum (foldl algebra.sum x xs) (foldl algebra.sum y ys)
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys
n : ℕ
a b : Variables n order.GrLex
x : ℕ
xs : List ℕ
p : List.length (x :: xs) = n
y : ℕ
ys : List ℕ
q : List.length (y :: ys) = n
size_eq : List.length (x :: xs) = List.length (y :: ys)
tails_size_eq : List.length xs = List.length ys
hh :
  foldl (fun a b => a + b) (x + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) x xs + foldl (fun a b => a + b) y ys
⊢ foldl (fun x y => x + y) (x + y) (zipWith (fun x y => x + y) xs ys) =
    foldl (fun x y => x + y) x xs + foldl (fun x y => x + y) y ys