∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y),
  CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr =
      CategoryTheory.CategoryStruct.id b.pt →
    ∀ (s : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)) (m : b.toCocone.pt ⟶ s.pt),
      (∀ (j : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
          CategoryTheory.CategoryStruct.comp (b.toCocone.ι.app j) m = s.ι.app j) →
        m =
          CategoryTheory.CategoryStruct.comp b.fst (CategoryTheory.Limits.BinaryCofan.inl s) +
            CategoryTheory.CategoryStruct.comp b.snd (CategoryTheory.Limits.BinaryCofan.inr s)