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