∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.snd h) = h