∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J PartOrdEmb}
  {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))}
  (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) (x y : PartOrdEmb.Limits.CoconePt hc),
  hc.desc ((CategoryTheory.forget PartOrdEmb).mapCocone s) x =
      hc.desc ((CategoryTheory.forget PartOrdEmb).mapCocone s) y →
    x = y