Nuprl - Proof: comp nat ind a

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

P:(

Prop). (

. (

. j<i

P(j))

P(i))

(

. P(i))

By:	Unfold `guard` 0 THEN RepD

Generated subgoal:

1 1. P : Prop
2. i:. (j:. j<i P(j)) P(i)
3. i :
P(i)
5 steps

About:

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