IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc find small greater bound11 1. k : [not for witness]
2. k List
{y:(k+1)| y greater-bounds nil }
By:
Def of <int> greater-bounds <int list> THEN Reduce Concl THEN Witness: 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
[not for witness]
{y:
