∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsSeparator G ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = 0) → f = 0