(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 2 2 1
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))
5. r : 
  Y((f,x. g(x,f)),r)  P(r)
By: DTerm (r+1) 4 THEN IfLab `main` (Thin 3) Auto

Generated subgoal:

1 3. r : 
4. Y(f,x. g(x,f))  (m:(r+1). P(m))
  Y((f,x. g(x,f)),r)  P(r)
3 steps

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

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