Nuprl Basics - Proof: sfa doc find small greater bound 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

1. k :

[not for witness]
2.

k List
3. u :

k
4. v :

k List
5. y :

(k+1)
6. y greater-bounds v [not for witness]

{y:

(k+1)| y greater-bounds u.v }

By:	Decide: u<y

Generated subgoals:

1 7. u<y
{y:(k+1)| y greater-bounds u.v }
6 steps

2 7. u<y
{y:(k+1)| y greater-bounds u.v }
7 steps

About:

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

1	7. u<y {y:(k+1)\| y greater-bounds u.v }	6 steps
2	7. u<y {y:(k+1)\| y greater-bounds u.v }	7 steps