IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
inv pre less eq n:. 0<n (m:. pre(m)pre(n) mn)
By:
RewriteOfThm
Thm* all
Thm* (n:hnum. implies(lt(0,n),all(m:hnum. equal(le(pre(m),pre(n)),le(m,n)))))
(SimpsetC [`hol_to_nuprl`;`bequal`])
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
n:
. 0<n 
(
pre(n) 
n:hnum. implies(lt(0,n),all(
