∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q]
  [inst_3 : CategoryTheory.Limits.HasPullback f g], Q g → (P (CategoryTheory.Limits.pullback.snd f g) ↔ P f)