∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ : B}
  {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryTheory.CategoryStruct.id b₀) (a : X ⟶ Y) {Z : ↑(F.obj b₀)}
  (h : (CategoryTheory.CategoryStruct.id (F.obj b₀)).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map a)
      (CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp a h)