∀ {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} (s : CategoryTheory.Limits.Cofork c.inr 0)
  {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.π