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

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

1. k :

[not for witness]
2. x :

k List

{y:

(k+1)| y greater-bounds x }

By:	ListInd Hyp:-1

Generated subgoals:

1 {y:(k+1)| y greater-bounds nil }
1 step

2 3. u : k
4. v : k List
5. {y:(k+1)| y greater-bounds v }
{y:(k+1)| y greater-bounds u.v }
15 steps

About:

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

1	{y:(k+1)\| y greater-bounds nil }	1 step
2	3. u : k 4. v : k List 5. {y:(k+1)\| y greater-bounds v } {y:(k+1)\| y greater-bounds u.v }	15 steps