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.