Nuprl - Proof: fincr formation 1 1

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

WellFnd{1}(

;u,v.(

i,j. i<j)(u,v))

By:	RW (RepeatC (UnfoldsC [`wellfounded`;`guard`;`so_apply`]) THENC AbReduceC) 0 THEN Analyze 0

Generated subgoal:

1 1. P : Prop
2. j:. (k:. k<j P(k)) P(j)
3. n :
P(n)
2 steps

About:

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