{X : AlgebraicGeometry.Scheme} →
  {motive : X.IsSeparated → Sort u_1} →
    (t : X.IsSeparated) →
      ((isSeparated_terminal_from : AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)) → motive ⋯) →
        motive t