Nuprl Basics - Proof: sfa doc find intlist great bound 1

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

1. x :

List

{y:

| y greater-bounds x }

By:	Def of y greater-bounds x

Generated subgoal:

1 {y:| i:||x||. x[i]<y }
17 steps

About:

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