(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 1 1 1
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))  (m:0. P(m))
By: ExtWith [] [VoidVoid]

Generated subgoals:

1   Y(f,x. g(x,f))  VoidVoid
Auto
2 4. x : 0
  Y((f,x. g(x,f)),x)  P(x)
1 step
3 1. P : Prop{k}
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  VoidVoid
  0  Type{1}
Auto

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

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