Nuprl - hol_arithmetic_4 LEMMAs for sub

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

Theorem	Name
Thm* x,n,m:. nx & mx (nnsub(x;n) = nnsub(x;m) n = m)	[sub_cancel]
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(n,p),le(m,p)) Thm* (p:hnum. (n:hnum. (m:hnum. ,equal Thm* (p:hnum. (n:hnum. (m:hnum. ,(equal(sub(p,n),sub(p,m)) Thm* (p:hnum. (n:hnum. (m:hnum. ,,equal(n,m))))))	[hsub_cancel]

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