unfold joinF.associatorRight
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ joinF.associatorRight ([] :: asss) = joinF.associatorRight asss
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ associatorRight.aux [] [] ([] :: asss) = associatorRight.aux [] [] asss