∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u_1, u_3} J]
  (i j : (AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).toLocallyRingedSpaceGlueData.J)
  (motive :
    (CategoryTheory.Limits.MultispanShape.prod
          (AlgebraicGeometry.Scheme.Cover.ulift
                  (AlgebraicGeometry.Scheme.Opens.iSupOpenCover fun i_1 =>
                    AlgebraicGeometry.Scheme.Hom.opensRange
                      (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R →
      Prop)
  (x :
    (CategoryTheory.Limits.MultispanShape.prod
        (AlgebraicGeometry.Scheme.Cover.ulift
                (AlgebraicGeometry.Scheme.Opens.iSupOpenCover fun i_1 =>
                  AlgebraicGeometry.Scheme.Hom.opensRange
                    (F.map i_1.snd.1))).gluedCover.toLocallyRingedSpaceGlueData.J).R),
  (∀ (k : ↥(F.obj ((equivShrink J).symm i)))
      (hk : k ∈ ⨆ i_1, AlgebraicGeometry.Scheme.Hom.opensRange (F.map i_1.snd.1)), motive ⟨k, hk⟩) →
    motive x