∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} {F : CategoryTheory.Functor C D} (X : C), P X → P.strictMap F (F.obj X)