no goals
ι : Type ?u.231477
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → α
a : α
l : List β
L : List (List β)
⊢ foldl f a (join (l :: L)) = foldl (foldl f) a (l :: L)
simp only [join, foldl_append, foldl_cons, foldl_join f (foldl f a l) L]