induction as₁
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List α
⊢ 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₂)
case nil
α : 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₂)

case cons
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  appendF.naturatorLax F tail✝ as₂ ≫ appendF.naturatorOplax F tail✝ as₂ =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor tail✝ ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)
⊢ appendF.naturatorLax F (head✝ :: tail✝) as₂ ≫ appendF.naturatorOplax F (head✝ :: tail✝) as₂ =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (head✝ :: tail✝) ++
        Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as₂)