dsimp [join]
α : Type u
as : List α
ass bss : List (List α)
⊢ join (as :: ass ++ bss) = join (as :: ass) ++ join bss
α : Type u
as : List α
ass bss : List (List α)
⊢ as ++ join (ass ++ bss) = as ++ join ass ++ join bss