{X : AlgebraicGeometry.Scheme} →
  {motive : AlgebraicGeometry.IsIntegral X → Sort u} →
    (t : AlgebraicGeometry.IsIntegral X) →
      ((nonempty : Nonempty ↥X) →
          (component_integral : ∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑(X.presheaf.obj (Opposite.op U))) →
            motive ⋯) →
        motive t