dsimp [join]
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (join (as :: ass)) = join (map (map f) (as :: ass))
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (as ++ join ass) = map f as ++ join (map (map f) ass)