conv => lhs; unfold joinF.associatorRight.aux
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorRight.aux as ass asss)
no goals