{X Y : AlgebraicGeometry.LocallyRingedSpace} →
  {motive : X.Hom Y → Sort u_1} →
    (t : X.Hom Y) →
      ((toHom : X.Hom Y.toPresheafedSpace) →
          (prop : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom.stalkMap x))) →
            motive { toHom := toHom, prop := prop }) →
        motive t