∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : CategoryTheory.Limits.HasKernels C] {X Z : C}
  (a : X ⟶ Z) (P : C) (f : Z ⟶ P) (haf : CategoryTheory.CategoryStruct.comp a f = 0) (Q : C) (g : Z ⟶ Q)
  (motive :
    { l //
        CategoryTheory.CategoryStruct.comp l
            (CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι a haf)) =
          CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.prod.lift f g) } →
      Prop)
  (x :
    { l //
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι a haf)) =
        CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.prod.lift f g) }),
  (∀
      (a' :
        CategoryTheory.Limits.kernel (CategoryTheory.Limits.prod.lift f g) ⟶
          (CategoryTheory.Limits.KernelFork.ofι a haf).pt)
      (ha' :
        CategoryTheory.CategoryStruct.comp a'
            (CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.ofι a haf)) =
          CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.prod.lift f g)),
      motive ⟨a', ha'⟩) →
    motive x