∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H),
  ℌ.ev_app =
    (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy F H).homEquiv.symm
      { app := fun x => CategoryTheory.MonoidalClosed.uncurry (ℌ.π x.2 x.1), naturality := ⋯ }