unfold joinF.associatorLeft.aux
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorLeft.aux [] (as :: ass) asss)
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorLeft.aux as ass asss)