dsimp [appendF.naturatorLax, appendF.naturatorOplax]
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ appendF.naturatorOplax F (a :: as₁) as₂ ≫ appendF.naturatorLax F (a :: as₁) as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a :: as₁ ++ as₂))
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
a : α
as₁ : List α
h_ind :
  appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂))
⊢ DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a) ≫ 𝟙 (Prefunctor.obj F.toPrefunctor a))
      (appendF.naturatorOplax F as₁ as₂ ≫ appendF.naturatorLax F as₁ as₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (as₁ ++ as₂)))