∀ (V : Type u_4) [inst : CategoryTheory.Category.{u_3, u_4} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {C : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X.obj ⟶[V] Y.obj)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X.obj) (X.obj ⟶[V] Y.obj))
        (CategoryTheory.eComp V X.obj X.obj Y.obj)) =
    CategoryTheory.CategoryStruct.id (X.obj ⟶[V] Y.obj)