Nuprl - hol_prim_rec LEMMAs for simp_rec

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

Theorem	Name
Thm* 'a:S, x:'a, f:('a'a), n:. fun:('a). simp_rec_rel(fun,x,f,n)	[simp_rec_exists]
cites the following:
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)))))	[hsimp_rec_exists]

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