∀ {B : Type u_2} [inst : CategoryTheory.Bicategory B] {C : Type u_9} [inst_1 : CategoryTheory.Bicategory C]
  {D : Type u_5} [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) {a b c : B} (x : a ⟶ b) (g : b ⟶ c),
  (F.comp G.toStrictlyUnitaryPseudofunctor).map (CategoryTheory.CategoryStruct.comp x g) =
    CategoryTheory.CategoryStruct.comp ((F.comp G.toStrictlyUnitaryPseudofunctor).map x)
      ((F.comp G.toStrictlyUnitaryPseudofunctor).map g)