all
  (b:hnum. all
  (b:hnum. (c:hnum. implies
  (b:hnum. (c:hnum. (le(c,b)
  (b:hnum. (c:hnum. ,all(a:hnum. equal(sub(a,sub(b,c)),sub(add(a,c),b))))))

None

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