Nuprl - Proof: complete nat ind with y 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: complete nat ind with y 1 1

1. P :

Prop
2. g :

. (

i. P(j))

P(i)

f,x. g(x,f))

(

. P(i))

By:	Assert (Y(f,x. g(x,f)) VoidVoid)

Generated subgoals:

1   Y(f,x. g(x,f))  VoidVoid
2 steps

2 3. Y(f,x. g(x,f))  VoidVoid
  Y(f,x. g(x,f))  (i:. P(i))
19 steps

About:

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

1	Y(f,x. g(x,f)) VoidVoid	2 steps
2	3. Y(f,x. g(x,f)) VoidVoid Y(f,x. g(x,f)) (i:. P(i))	19 steps