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

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

1. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3. i :

zz,i:

. i<zz

P(i)

By:	p. let i mvt (var_of_hyp -2 p) , let ip1 mk_add_term i 1 in ((DTerm ip1 -1) THEN (DTerm i -1)) p

Generated subgoals:

1   i+1
6 steps

2   i
1 step

3 4. i<i+1  P(i)
  P(i)
3 steps

About:

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