∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y A : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q],
  CategoryTheory.IsPushout f g inl inr → Q f → (P inl ↔ P g)