∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ≅ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ≅ G.obj CategoryTheory.Limits.WalkingReflexivePair.one),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁.hom =
      CategoryTheory.CategoryStruct.comp e₀.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) →
    CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁.inv =
      CategoryTheory.CategoryStruct.comp e₀.inv (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)