∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasCoend F']
  (f : F ⟶ F') {F'' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_4 : CategoryTheory.Limits.HasCoend F''] (g : F' ⟶ F'') {Z : C} (h : CategoryTheory.Limits.coend F'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map (CategoryTheory.CategoryStruct.comp f g)) h