∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X))
      ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)