∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {S : CategoryTheory.Sieve X}
  (motive : (∃ R ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X, R ≤ S.arrows) → Prop)
  (x : ∃ R ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X, R ≤ S.arrows),
  (∀ (R : CategoryTheory.Presieve X) (hR : R ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X)
      (hle : R ≤ S.arrows), motive ⋯) →
    motive x