∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X}
  (k : CategoryTheory.IsKernelPair f a b) (r : CategoryTheory.RegularEpi f)
  (ht :
    CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.IsPullback.isLimit k).lift (CategoryTheory.Limits.PullbackCone.mk r.left r.right ⋯)) a =
      r.left)
  (kt :
    CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.IsPullback.isLimit k).lift (CategoryTheory.Limits.PullbackCone.mk r.left r.right ⋯)) b =
      r.right)
  (s : CategoryTheory.Limits.Cofork a b) (m : (CategoryTheory.Limits.Cofork.ofπ f ⋯).pt ⟶ s.pt),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.ofπ f ⋯).π m = s.π →
    m = CategoryTheory.Limits.Cofork.IsColimit.desc r.isColimit s.π ⋯