∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁)
  {Z : F.obj b₀ ⟶ F.obj b₁}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id b₀)) (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).inv (F.map f)) h)