∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y), CategoryTheory.Limits.Cofork.π c.inlCokernelCofork = c.snd