It is necessary when ``proving'' recursive or mutually recursive
tactics to introduce embedded instances of theorems which have not yet
been proved. The rule infix introduction commands do check for
existence of theorems, so it is necessary to use the `
declarepretheorem` command to signal the future intention of proving
a theorem with the recursively introduced name.

Fri Sep 5 16:28:58 MDT 1997