Documentation Request: declare-refinement

What version of Racket are you using?

v6.12

What program did you run?

#lang typed/racket #:with-refinements

(: seven? (-> Integer Boolean))
(define (seven? x)
  (equal? x 7)
  )

(declare-refinement even?)
(declare-refinement seven?)

What should have happened?

This might be a documentation request, but I'm not sure how to use (declare-refinement) from the documentation. The only use of it is in the Typed Racket codebase is in a unit test with even?, which does seem to work.

The documentation only says that the identifier should be a predicate, but even? appears to be annotated with some additional propositions.

[even? (-> -Int B : (-PS (-not-type 0 -One) (-not-type 0 -Zero)))]

How should one annotate an arbitrary predicate so that it is usable as a refinement type?

If you got an error message, please include it here.

 mismatch in proposition
  expected: ((: x (Refinement Integer seven?)) | (! x (Refinement Integer seven?)))
  given: (Top | Top)
  in: (equal? x 7)

Start with the documentation entry for declare-refinement and the Typed Racket unit test using even?, then compare them with the shown seven? example and its type-checker error. Document how an arbitrary predicate should be annotated for use as a refinement type, including the relevant proposition behavior, and ensure the example's expected usage is clear.