∀ (B : Type u_1) [inst : CategoryTheory.Bicategory B] (C : Type u_2) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.associator f g h).hom.2
      (CategoryTheory.Bicategory.associator f g h).hom.1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.Prod.mkHom f.2 f.1) (CategoryTheory.Prod.mkHom g.2 g.1)
            (CategoryTheory.Prod.mkHom h.2 h.1)).hom
        (CategoryTheory.eqToHom ⋯))