no goals
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
l : List β₁
init : α
⊢ foldl g init (map f l) = foldl (fun x y => g x (f y)) init l
induction l generalizing init <;> simp [*]