1. n : 
2. n1:. n1<n  (f:{f:()| x:. f(x) }. mu(f) = n1  f(mu(f)))
3. f : {f:()| x:. f(x) }
4. mu(f) = n
5. f(0)
  f(1+mu(x.f(1+x)))

By:	FwdThru:  Thm* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) } on [ f(0) ] THEN (Inst: Hyp:2 Using:[mu(x.f(1+x)) | x.f(1+x)] THEN (Reduce Hyp:-1))

1

6. (x.f(1+x))  {f:()| x:. f(x) }   mu(x.f(1+x))<n

2 steps

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