rw [h_ind, Category.id_comp]
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorLax F G as ≫ mapF.compositorOplax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))