dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
⊢ joinF.unitorRightLax (a :: as) ≫ joinF.unitorRightOplax (a :: as) = 𝟙 (a :: as)
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorRightLax as ≫ joinF.unitorRightOplax as) = DVect2.cons (𝟙 a) (𝟙 as)