rw [Nat.add_assoc]
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
⊢ foldl (fun a b => a + b) (init₁ + x + init₂ + y) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
open_init₂ : init₂ + (x + y) = x + init₂ + y
size_eq : List.length xs = List.length ys
res :
  foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys
⊢ foldl (fun a b => a + b) (init₁ + x + (init₂ + y)) (zipWith (fun a b => a + b) xs ys) =
    foldl (fun a b => a + b) (init₁ + x) xs + foldl (fun a b => a + b) (init₂ + y) ys