∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {B X : C} {f : X ⟶ B} (hf : CategoryTheory.RegularEpi f)
  {W : C} (x : X ⟶ W)
  (x_1 :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ X),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ x = CategoryTheory.CategoryStruct.comp g₂ x),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.ofπ f ⋯).π
      (CategoryTheory.Limits.Cofork.IsColimit.desc hf.isColimit x ⋯) =
    x