∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C] (f : CategoryTheory.Arrow C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.cokernel.π f.hom) ⋯).π
      (CategoryTheory.Iso.refl (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.cokernel.π f.hom) ⋯).pt).hom =
    CategoryTheory.Limits.Cofork.π
      ((CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.coker.π C) ⋯).map
        ((CategoryTheory.evaluation (CategoryTheory.Arrow C) C).obj f))