∀ (x : AlgebraicGeometry.Scheme) (x_1 : AlgebraicGeometry.Scheme.forget.obj x) (w : CategoryTheory.Presieve x)
  (motive : (∃ Y g, CategoryTheory.Presieve.map AlgebraicGeometry.Scheme.forget w g ∧ x_1 ∈ Set.range g) → Prop)
  (x_2 : ∃ Y g, CategoryTheory.Presieve.map AlgebraicGeometry.Scheme.forget w g ∧ x_1 ∈ Set.range g),
  (∀ (Y : Type u_1) (u : Y ⟶ AlgebraicGeometry.Scheme.forget.obj x)
      (hu : CategoryTheory.Presieve.map AlgebraicGeometry.Scheme.forget w u) (hmem : x_1 ∈ Set.range u), motive ⋯) →
    motive x_2