dsimp [join]
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (join (as :: asss)) = join (map join (as :: asss))
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (as ++ join asss) = join as ++ join (map join asss)