induction ass
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (ass :: asss))
case nil
α : 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)
⊢ joinF.associatorLeft ([] :: asss) ≫ joinF.associatorRight ([] :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor ([] :: asss))

case cons
α : 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)
head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  joinF.associatorLeft (tail✝ :: asss) ≫ joinF.associatorRight (tail✝ :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (tail✝ :: asss))
⊢ joinF.associatorLeft ((head✝ :: tail✝) :: asss) ≫ joinF.associatorRight ((head✝ :: tail✝) :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor ((head✝ :: tail✝) :: asss))