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