∀ (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) (W X Y Z : P.FullSubcategory),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (W.obj ⟶[V] X.obj) (X.obj ⟶[V] Y.obj) (Y.obj ⟶[V] Z.obj)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W.obj X.obj Y.obj)
          (Y.obj ⟶[V] Z.obj))
        (CategoryTheory.eComp V W.obj Y.obj Z.obj)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W.obj ⟶[V] X.obj) (CategoryTheory.eComp V X.obj Y.obj Z.obj))
      (CategoryTheory.eComp V W.obj X.obj Z.obj)