∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {c : CategoryTheory.Limits.BinaryBicone X Y} (i : CategoryTheory.Limits.IsColimit c.toCocone)
  (s : CategoryTheory.Limits.Cofork c.inr 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c.inrCokernelCofork)
        (CategoryTheory.CategoryStruct.comp c.inl s.π) =
      s.π ∧
    ∀
      {m :
        ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj c.inrCokernelCofork.pt).obj
            CategoryTheory.Limits.WalkingParallelPair.one ⟶
          ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
            CategoryTheory.Limits.WalkingParallelPair.one},
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c.inrCokernelCofork) m = s.π →
        m = CategoryTheory.CategoryStruct.comp c.inl s.π