∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y S : C} (f : X ⟶ S)
  (g : Y ⟶ S) [inst_1 : CategoryTheory.Limits.HasPullback f g] [P.IsStableUnderBaseChangeAlong f],
  P g → P (CategoryTheory.Limits.pullback.fst f g)