∀ {B : Type u_2} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (P.fullsubcategory.map₂ η) { toFunctor := (P.prop b).ι })
      (CategoryTheory.Iso.refl
          (CategoryTheory.CategoryStruct.comp (P.fullsubcategory.map g) { toFunctor := (P.prop b).ι })).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (CategoryTheory.CategoryStruct.comp (P.fullsubcategory.map f) { toFunctor := (P.prop b).ι })).hom
      (CategoryTheory.Bicategory.whiskerLeft { toFunctor := (P.prop a).ι } (F.map₂ η))