simp
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorLeft (([] :: ass) :: asss) ≫ joinF.associatorRight (([] :: ass) :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (([] :: ass) :: asss))
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙
      (Prefunctor.obj joinF.toPrefunctor ass ++
        Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF).toPrefunctor asss))