no goals
ι : Type ?u.230724
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a (b :: l) = a
rw [foldl_cons, hf b, foldl_fixed' hf l]