{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.IsLimit c.toCone → CategoryTheory.Limits.IsLimit c.fstKernelFork