∀ (B : Type u_5) [inst : CategoryTheory.Bicategory B] (C : Type u_6) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d e : CategoryTheory.Pseudofunctor B C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight
        (CategoryTheory.Pseudofunctor.StrongTrans.associator f g h).hom i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Pseudofunctor.StrongTrans.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
        (CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft f
          (CategoryTheory.Pseudofunctor.StrongTrans.associator g h i).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.StrongTrans.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
      (CategoryTheory.Pseudofunctor.StrongTrans.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom