Nuprl - hol_arithmetic_4 LEMMAs for sub

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

Theorem	Name
Thm* b,c:. cb (a:. nnsub(a;nnsub(b;c)) = nnsub(a+c;b))	[sub_sub]
cites the following:
Thm* all Thm* (b:hnum. all Thm* (b:hnum. (c:hnum. implies Thm* (b:hnum. (c:hnum. (le(c,b) Thm* (b:hnum. (c:hnum. ,all Thm* (b:hnum. (c:hnum. ,(a:hnum. equal(sub(a,sub(b,c)),sub(add(a,c),b))))))	[hsub_sub]

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