∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair F).hom.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero =>
      CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
    | CategoryTheory.Limits.WalkingReflexivePair.one =>
      CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.one)