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