case cons a as h_ind =>
  dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
  rw [Category.id_comp, h_ind]
  rfl
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ joinF.unitorRightOplax (a :: as) ≫ joinF.unitorRightLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor (a :: as))
no goals