∀ {Q : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {X Y : AlgebraicGeometry.Scheme} {x : AlgebraicGeometry.IsAffine Y} (f : X ⟶ Y)
  (motive : AlgebraicGeometry.affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f → Prop)
  (x : AlgebraicGeometry.affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f),
  (∀ (hX : AlgebraicGeometry.IsAffine X) (hf : Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f))),
      motive ⋯) →
    motive x