∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} [inst_2 : SizeOf C] (bicone : CategoryTheory.Limits.BinaryBicone P Q) (isBilimit : bicone.IsBilimit),
  sizeOf { bicone := bicone, isBilimit := isBilimit } = 1 + sizeOf bicone + sizeOf isBilimit