∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {f : X ⟶ Y} {W : C} (g : W ⟶ X)
  (lift : {W' : C} → (g' : W' ⟶ X) → CategoryTheory.CategoryStruct.comp g' f = 0 → (W' ⟶ W)),
  (∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0) (m : W' ⟶ W),
      CategoryTheory.CategoryStruct.comp m g = g' → m = lift g' eq') →
    ∀ (s : CategoryTheory.Limits.KernelFork f)
      (m :
        ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
            CategoryTheory.Limits.WalkingParallelPair.zero ⟶
          W),
      CategoryTheory.CategoryStruct.comp m g = CategoryTheory.Limits.Fork.ι s →
        m = lift (CategoryTheory.Limits.Fork.ι s) ⋯