rw [h_ind, Category.id_comp]
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  mapF.unitorOplax as ≫ mapF.unitorLax as = 𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (mapF.unitorOplax as ≫ mapF.unitorLax as) =
    DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (𝟭 α)).toPrefunctor as))
no goals