no goals
ι : Type ?u.133368
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
L : List (List α)
⊢ map f (join L) = join (map (map f) L)
induction L <;> [rfl; simp only [*, join, map, map_append]]