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))
  Y(f,x. g(x,f))  (m:n. P(m))

By:	ExtWith [`r'] [VoidVoid]

1

7. r : n   Y((f,x. g(x,f)),r)  P(r)

6 steps

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