∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q : C} {bicone : CategoryTheory.Limits.BinaryBicone P Q} {isBilimit : bicone.IsBilimit}
  {bicone_1 : CategoryTheory.Limits.BinaryBicone P Q} {isBilimit_1 : bicone_1.IsBilimit},
  { bicone := bicone, isBilimit := isBilimit } = { bicone := bicone_1, isBilimit := isBilimit_1 } →
    bicone = bicone_1 ∧ isBilimit ≍ isBilimit_1