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

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

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 3

1. P :

Prop
2.

i:

. (

j:

. j<i

P(j))

P(i)
3. zz :

4. 0<zz
5.

i:

. i<zz-1

P(i)

Type{1}

By:

MemEqCD

Generated subgoals:

None

About:

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

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