∀ (X : AlgebraicGeometry.Scheme),
  { I₀ := X.AffineZariskiSite, X := fun U => ↑↑U, f := fun U => (↑U).ι }.presieve₀ ∈
    (AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion).coverings X