∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {ι : Type u_1} [inst_1 : LinearOrder ι]
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C}
  (c : CategoryTheory.Limits.Multicofork I) (hc : CategoryTheory.Limits.IsColimit c) (h : I.SymmStruct)
  (s : CategoryTheory.Limits.Multicofork I.toLinearOrder) (m : c.toLinearOrder.pt ⟶ s.pt),
  (∀ (i : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R),
      CategoryTheory.CategoryStruct.comp (c.toLinearOrder.π i) m = s.π i) →
    m = hc.desc (s.ofLinearOrder h)