∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (x : (E.sigmaOfIsColimit hc hd).multicospanShape.R), x = x