∀ (B : Type u_5) [inst : CategoryTheory.Bicategory B] (C : Type u_6) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : CategoryTheory.OplaxFunctor B C} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Oplax.OplaxTrans.associator f (CategoryTheory.CategoryStruct.id b) g).hom
      (CategoryTheory.Oplax.OplaxTrans.whiskerLeft f (CategoryTheory.Oplax.OplaxTrans.leftUnitor g).hom) =
    CategoryTheory.Oplax.OplaxTrans.whiskerRight (CategoryTheory.Oplax.OplaxTrans.rightUnitor f).hom g