∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (η : CategoryTheory.Oplax.StrongTrans F G) {a : B} {a' : CategoryTheory.Cat} (f : G.obj a ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (f.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app X))
      (f.toFunctor.map ((G.mapId a).toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp (f.toFunctor.map ((η.app a).toFunctor.map ((F.mapId a).toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (f.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app a).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X))))
        (f.toFunctor.map (CategoryTheory.CategoryStruct.id ((η.app a).toFunctor.obj X))))