∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C),
  CategoryTheory.Limits.reflexiveCoforkEquivCofork F =
    (CategoryTheory.Functor.Final.coconesEquiv CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair
            F).symm.trans
      (CategoryTheory.Limits.Cocones.precomposeEquivalence
          (CategoryTheory.Limits.diagramIsoParallelPair
            (CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.comp F))).symm