∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) {Z : C} (l : Z ⟶ Y) (i : X ≅ Z),
  CategoryTheory.CategoryStruct.comp i.hom l = f →
    ∀ {s : CategoryTheory.Limits.CokernelCofork f},
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.Cofork.π s) = 0