∀ {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)
  {h₃ :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
      CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)},
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
    CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)