∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : P.IsMonoidalClosed] (X : P.FullSubcategory) ⦃X_1 Y : P.FullSubcategory⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id P.FullSubcategory).map f)
      (CategoryTheory.ObjectProperty.homMk ((CategoryTheory.ihom.coev X.obj).app Y.obj)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ObjectProperty.homMk ((CategoryTheory.ihom.coev X.obj).app X_1.obj))
      (((CategoryTheory.MonoidalCategory.tensorLeft X).comp (P.lift (P.ι.comp (CategoryTheory.ihom X.obj)) ⋯)).map f)