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)