The rewrite package must have access to several kinds of lemmas in order to construct justifications for rewrites. This section describes those lemmas.
Note that for order relations, one only needs lemmas for one direction. For example, one doesn't require both the lemma
and
If Nuprl finds a lemma missing in the course of constructing a rewrite justification it prints out an error message suggesting the kind and structure of the missing lemma. After entering it, you need to evaluate the function
initialize_rw_lemma_caches : unit -> unit
on argument () in the ML Top Loop ; for efficiency reasons, the rewrite code caches information about these lemmas and hasn't been set up yet to automatically update caches after changes to the available lemmas in the library.