∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (j : CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).ι j =
    CategoryTheory.Limits.WalkingPair.casesOn j b.inl b.inr