Nuprl - Proof: comp nat ind tp 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. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3.

zz,i:

. i<zz

P(i)

By:	p.Thin (get_int_arg `hn` p) p

Generated subgoal:

1 zz,i:. i<zz P(i)
19 steps

About:

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