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