∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} 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)}
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{u_1, u_2} D] (H : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp ((F.comp H).map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
      (H.map e₁) =
    CategoryTheory.CategoryStruct.comp (H.map e₀)
      ((G.comp H).map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)