∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty},
  Q.IsLocal → P = AlgebraicGeometry.targetAffineLocally Q → AlgebraicGeometry.HasAffineProperty P Q