∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {c : CategoryTheory.Limits.Bicone f},
  Subsingleton c.IsBilimit