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