∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor D C) [F.Full] {G : C}
  [CategoryTheory.Projective G],
  CategoryTheory.IsSeparator G →
    (∀ (X : D), ∃ p, CategoryTheory.Epi p) → (F.comp (CategoryTheory.preadditiveCoyonedaObj G)).Full