'a:S. 
  all
  (fun:hnum
  ( 'a. all
  ( 'a. (x:'a. all
  ( 'a. (x:'a. (f:'a  'a. all
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. equal
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. (simp_rec_rel(fun,x,f,n)
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,and
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,(equal(fun(0),x)
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,all
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. implies
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. (lt(m,n)
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,equal
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,(fun(suc(m))
  ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,,f(fun(m)))))))))))

None

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