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