∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T)
  [inst_1 : CategoryTheory.Limits.HasPullbacks T] [P.IsStableUnderComposition] [P.ContainsIdentities]
  [inst_4 : P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] {X Y : T} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MorphismProperty.Over.pullback P ⊤ f)