no goals
ι : Type ?u.232055
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → β
a : β
l : List α
L : List (List α)
⊢ foldr f a (join (l :: L)) = foldr (fun l b => foldr f b l) a (l :: L)
simp only [join, foldr_append, foldr_join f a L, foldr_cons]