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

case cons
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
head✝ : α
tail✝ : List α
tail_ih✝ :
  joinF.associatorRight ((tail✝ :: ass) :: asss) ≫ joinF.associatorLeft ((tail✝ :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((tail✝ :: ass) :: asss))
⊢ joinF.associatorRight (((head✝ :: tail✝) :: ass) :: asss) ≫ joinF.associatorLeft (((head✝ :: tail✝) :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (((head✝ :: tail✝) :: ass) :: asss))