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). Thm* simp_rec(x,f,0) = x & (m:. simp_rec(x,f,m+1) = f(simp_rec(x,f,m)))	[simp_rec_thm]
cites the following:
Thm* 'a:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a 'a. and Thm* (x:'a. (f:'a 'a. (equal(simp_rec(x,f,0),x) Thm* (x:'a. (f:'a 'a. ,all Thm* (x:'a. (f:'a 'a. ,(m:hnum. equal Thm* (x:'a. (f:'a 'a. ,(m:hnum. (simp_rec(x,f,suc(m)) Thm* (x:'a. (f:'a 'a. ,(m:hnum. ,f(simp_rec(x,f,m)))))))	[hsimp_rec_thm]

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