Nuprl - Proof: nat ind tp 1 1 1 2

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

1. P :

Prop
2. P(0)
3.

. P(i-1)

P(i)

P(0)

By:

Analyze 0

Generated subgoals:

1 4. 00
  P(0)
2 steps

2 1. P : Prop{k}
2. P(0)
3. i:. P(i-1)  P(i)
  (00)  Prop{1}
1 step

About:

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

1	4. 00 P(0)	2 steps
2	1. P : Prop{k} 2. P(0) 3. i:. P(i-1) P(i) (00) Prop{1}	1 step