case cons ass asss h_indsss =>
  induction ass 
  case nil => simp; exact h_indsss
  case cons as ass h_indss =>
    induction as
    case nil => simp; exact h_indss
    case cons a as h_inds => simp; rw [h_inds]; rfl
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
no goals