rw [Nat.add_right_comm, Nat.add_comm]
case open_init₂
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
x : ℕ
xs : List ℕ
y : ℕ
ys : List ℕ
h : List.length (x :: xs) = List.length (y :: ys)
⊢ init₂ + (x + y) = x + init₂ + y

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
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + 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
⊢ foldl (fun a b => a + b) (init₁ + init₂ + (x + 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