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

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