(24steps total) PrintForm Definitions int 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: complete nat ind with y 1 1 1
1. P : Prop
2. g : i:. (j:i. P(j))  P(i)
  Y(f,x. g(x,f))  VoidVoid
By: Rewrite (HigherC YUnrollC) 0 THEN Reduce 0

Generated subgoal:

1   (x.g(x,Y(f,x. g(x,f))))  VoidVoid
1 step

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

(24steps total) PrintForm Definitions int 1 Sections StandardLIB Doc