Nuprl Basics - Proof: sfa doc find small greater bound

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

. x:(

k List)

{y:

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

By:

Analyze

Generated subgoal:

1 1. k : [not for witness]
2. x : k List
{y:(k+1)| y greater-bounds x }
17 steps

About:

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