case nil =>
  dsimp [appendF.naturatorLax, appendF.naturatorOplax]
  rw [Category.id_comp (X:=(mapF.obj F).obj as₂)]
  rfl
α : 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₂)
no goals