Nuprl - Proof: fincr wf2 1 3

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

WellFnd{[1]}(

;u,v.(

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

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

Generated subgoal:

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

About:

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