∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] {F : CategoryTheory.Functor C D}
  (motive : F.EssImageSubcategory → Prop) (x : F.EssImageSubcategory),
  (∀ (obj : D) (hY : F.essImage obj), motive { obj := obj, property := hY }) → motive x