(P,g. Y(f,x. g(x,f)))
   (P:(Prop). (i:. (j:i. P(j))  P(i))  (i:. P(i)))

1

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

22 steps

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