∀ {B : Type u_2} [inst : CategoryTheory.Bicategory B] {C : Type u_6} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G)
  (θ : CategoryTheory.Oplax.StrongTrans G H) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.Bicategory.associator (F.map f) (η.toOplax.app b) (θ.toOplax.app b)).symm ≪≫
        CategoryTheory.Bicategory.whiskerRightIso (η.naturality f) (θ.app b) ≪≫
          CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b) ≪≫
            CategoryTheory.Bicategory.whiskerLeftIso (η.app a) (θ.naturality f) ≪≫
              (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).symm).hom =
    (η.toOplax.vcomp θ.toOplax).naturality f