no goals
α : Type u_1
β : Type u_2
l : List α
acc : Array β
F : Array β → α → Array β
G : α → List β
H : ∀ (acc : Array β) (a : α), (F acc a).data = acc.data ++ G a
⊢ (List.foldl F acc l).data = acc.data ++ List.bind l G
induction l generalizing acc <;> simp [*, List.bind]