Nuprl - Proof: complete nat ind with y 1 1 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 1

1. P :

Prop
2. g :

. (

i. P(j))

P(i)

(

x.g(x,Y(

f,x. g(x,f))))

Void

By:

Analyze

Generated subgoals:

None

About:

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