{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.IsProper f → Sort u_1} →
      (t : AlgebraicGeometry.IsProper f) →
        ([toIsSeparated : AlgebraicGeometry.IsSeparated f] →
            [toUniversallyClosed : AlgebraicGeometry.UniversallyClosed f] →
              [toLocallyOfFiniteType : AlgebraicGeometry.LocallyOfFiniteType f] → motive ⋯) →
          motive t