dsimp [joinF.unitorLeftLax, joinF.unitorLeftOplax]
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ joinF.unitorLeftOplax (a :: as) ≫ joinF.unitorLeftLax (a :: as) =
    𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor (a :: as))
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor (a :: as)))