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

By:	Assert (n:. Y(f,x. g(x,f))  (m:n. P(m)))

1	n:. Y(f,x. g(x,f))  (m:n. P(m))	13 steps
2	4. n:. Y(f,x. g(x,f))  (m:n. P(m))   Y(f,x. g(x,f))  (i:. P(i))	5 steps

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