∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g),
  c.op.π.app CategoryTheory.Limits.WalkingParallelPair.one = (c.ι.app CategoryTheory.Limits.WalkingParallelPair.zero).op