Nuprl - Proof: complete nat ind with y 1 1 2 1

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. P :

Prop
2. g :

. (

i. P(j))

P(i)
3. Y(

f,x. g(x,f))

Void

. Y(

f,x. g(x,f))

(

n. P(m))

By:

Analyze 0

Generated subgoal:

1 4. n :
Y(f,x. g(x,f)) (m:n. P(m))
12 steps

About:

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