match l₁, l₂ with
  | [], []       => simp
  | x::xs, y::ys => simp
                    have open_init₂ : init₂ + (x + y) = x + init₂ + y
                    rw [Nat.add_right_comm, Nat.add_comm] 
                    rw [Nat.add_assoc, open_init₂, ← Nat.add_assoc, ←Nat.add_assoc]
                    have size_eq : xs.length = ys.length
                    simp at h
                    exact h
                    have res := zipWith_to_fold (init₁ + x) (init₂ + y) xs ys size_eq
                    simp [sum] at res
                    rw [Nat.add_assoc]
                    exact res
init₁ init₂ : ℕ
l₁ l₂ : List ℕ
h : List.length l₁ = List.length l₂
⊢ foldl (fun a b => a + b) (init₁ + init₂) (zipWith (fun a b => a + b) l₁ l₂) =
    foldl (fun a b => a + b) init₁ l₁ + foldl (fun a b => a + b) init₂ l₂
no goals