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