{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X Y : AlgebraicGeometry.Scheme} →
    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X →
      (f : Y ⟶ X) →
        autoParam (P f) AlgebraicGeometry.Scheme.Cover.add._auto_1 →
          AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X