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

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

Prop
2.

. (

. j<i

P(j))

P(i)

zz,i:

. i<zz

P(i)

By:

Analyze 0

Generated subgoals:

1 3. zz :
  i:. i<zz  P(i)
17 steps

2 1. P : Prop{k}
2. i:. (j:. j<i  P(j))  P(i)
    Type{1}
1 step

About:

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

1	3. zz : i:. i<zz P(i)	17 steps
2	1. P : Prop{k} 2. i:. (j:. j<i P(j)) P(i) Type{1}	1 step