induction as
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
as : List α
⊢ mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
case nil
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorLax F G [] ≫ mapF.compositorOplax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor [])

case cons
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  mapF.compositorLax F G tail✝ ≫ mapF.compositorOplax F G tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor tail✝)
⊢ mapF.compositorLax F G (head✝ :: tail✝) ≫ mapF.compositorOplax F G (head✝ :: tail✝) =
    𝟙
      (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
        (head✝ :: tail✝))