Nuprl Basics - Proof: sfa doc find small greater bound 1 2 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc find small greater bound 1 2 1 2 1

1. k :

k List
3. u :

k
4. v :

k List
5. y :

(k+1)
6. y greater-bounds v
7.

u<y

u+1 greater-bounds u.v

By:	Reduce Hyp:-1

Generated subgoal:

1 u+1 greater-bounds u.v
5 steps

About:

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