∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {B : C} {α : Type u_3} (X : α → C)
  (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (π : (a : α) → X a ⟶ B) {W : C}
  (e : c.pt ⟶ W) (m : (CategoryTheory.Limits.Cofan.mk B π).pt ⟶ W),
  CategoryTheory.CategoryStruct.comp (hc.desc (CategoryTheory.Limits.Cofan.mk B π)) m = e →
    ∀ {Z : C} (x x_1 : α) (x_2 : Z ⟶ X x) (x_3 : Z ⟶ X x_1),
      CategoryTheory.CategoryStruct.comp x_2 (π x) = CategoryTheory.CategoryStruct.comp x_3 (π x_1) →
        CategoryTheory.CategoryStruct.comp x_2
            ((fun a => CategoryTheory.CategoryStruct.comp (c.ι.app { as := a }) e) x) =
          CategoryTheory.CategoryStruct.comp x_3
            ((fun a => CategoryTheory.CategoryStruct.comp (c.ι.app { as := a }) e) x_1)