∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y Y' : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ A ⟹ Y) (g : Y ⟶ Y') {Z : C} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom A).map g))) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f)
      (CategoryTheory.CategoryStruct.comp g h)