{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.IsSeparated f → Sort u_1} →
      ((isClosedImmersion_diagonal : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)) →
          motive ⋯) →
        (t : AlgebraicGeometry.IsSeparated f) → motive t