dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
α : 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))
α : 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)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorRightOplax as ≫ joinF.unitorRightLax as) =
    𝟙
      (Prefunctor.obj singletonF.toPrefunctor a ++
        Prefunctor.obj joinF.toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor as))