Nuprl - Proof: fincr wf 1 3 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fincr wf 1 3 1

1. P :

Prop
2.

. (

. k<j

P(k))

P(j)
3. n :

P(n)

By:	CompNatInd -1

Generated subgoal:

1 4. n1:. n1<n P(n1)
P(n)
2 steps

About:

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