Nuprl - Proof: comp nat ind tp 1 1 1 1 1 1 2 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp nat ind tp 1 1 1 1 1 1 2 1 2

1. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3. zz :

4. 0<zz
5.

. i<zz-1

P(i)
6. i :

7. i<zz
8.

i1:

. i1<i

P(i1)

P(i)

By:	OnHyps [-2;-3;-3;-3] Thin

Generated subgoal:

1 3. i :
4. i1:. i1<i P(i1)
P(i)
1 step

About:

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