'a:S, x:'a, f:('a'a), n:. fun:('a). simp_rec_rel(fun,x,f,n)

By:

RewriteOfThm Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. all Thm* (x:'a. (f:'a  'a. (n:hnum. exists Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. simp_rec_rel Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. (fun Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. ,x Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. ,f Thm* (x:'a. (f:'a  'a. (n:hnum. (fun:hnum  'a. ,n))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html