∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : C},
  CategoryTheory.IsCoseparator G →
    ∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
      (∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g