1. P : Prop
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  VoidVoid
4. n : 
5. 0<n
6. Y(f,x. g(x,f))  (m:(n-1). P(m))
7. r : n
  Y((f,x. g(x,f)),r)  P(r)

1	8. r = n-1   Y((f,x. g(x,f)),r)  P(r)	4 steps
2	8. r = n-1   Y((f,x. g(x,f)),r)  P(r)	1 step

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