1. P : Prop
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  VoidVoid
4. n:. Y(f,x. g(x,f))  (m:n. P(m))
  Y(f,x. g(x,f))  (i:. P(i))

By:	ExtWith [`r'] [VoidVoid]

1

5. r :    Y((f,x. g(x,f)),r)  P(r)

4 steps

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