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