∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X}
  (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (hc.desc d) h) =
    CategoryTheory.CategoryStruct.comp (d.inj i) h