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