IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc find greater bound stupidly extr eq (k,x. k) = ext{sfa_doc_find_greater_bound_stupidly}
By:
Compute k,x. k * ext{sfa_doc_find_greater_bound_stupidly}
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html