∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {f : X ⟶ Y} (hf : CategoryTheory.NormalEpi f) {X' Y' : C} {f' : X' ⟶ Y'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Cofork.π
        ((CategoryTheory.Limits.Cocones.precompose
              (CategoryTheory.Limits.parallelPair.ext
                  (CategoryTheory.Iso.refl
                    ((CategoryTheory.Limits.parallelPair CategoryTheory.NormalEpi.g 0).obj
                      CategoryTheory.Limits.WalkingParallelPair.zero))
                  (CategoryTheory.Arrow.leftFunc.mapIso e) ⋯ ⋯).inv).obj
          (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)))
      (CategoryTheory.Arrow.rightFunc.mapIso e).hom =
    CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.CokernelCofork.ofπ f' ⋯)