∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g],
  ∃ s,
    CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B ∧
      CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B