Nuprl - hol_arithmetic_4 LEMMAs for cancel

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

Theorem	Name
Thm* x,n,m:. xn & xm (nnsub(n;x) = nnsub(m;x) n = m)	[cancel_sub]
cites the following:
Thm* all Thm* (p:hnum. all Thm* (p:hnum. (n:hnum. all Thm* (p:hnum. (n:hnum. (m:hnum. implies Thm* (p:hnum. (n:hnum. (m:hnum. (and(le(p,n),le(p,m)) Thm* (p:hnum. (n:hnum. (m:hnum. ,equal Thm* (p:hnum. (n:hnum. (m:hnum. ,(equal(sub(n,p),sub(m,p)) Thm* (p:hnum. (n:hnum. (m:hnum. ,,equal(n,m))))))	[hcancel_sub]

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