∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} {hom : A.pt ⟶ B.pt}
  {wfst :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam}
  {wsnd :
    autoParam (CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam}
  {winl :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam}
  {winr :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam}
  {hom_1 : A.pt ⟶ B.pt}
  {wfst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 B.fst = A.fst)
      CategoryTheory.Limits.BinaryBiconeMorphism.wfst._autoParam}
  {wsnd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp hom_1 B.snd = A.snd)
      CategoryTheory.Limits.BinaryBiconeMorphism.wsnd._autoParam}
  {winl_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.inl hom_1 = B.inl)
      CategoryTheory.Limits.BinaryBiconeMorphism.winl._autoParam}
  {winr_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.inr hom_1 = B.inr)
      CategoryTheory.Limits.BinaryBiconeMorphism.winr._autoParam},
  { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr } =
      { hom := hom_1, wfst := wfst_1, wsnd := wsnd_1, winl := winl_1, winr := winr_1 } →
    hom = hom_1