IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hnum axiom
'a:S.
all
(
e:'a. all
(e:'a. (f:'a 
hnum 'a. exists_unique
(e:'a. (f:'a hnum 'a. (fn1:hnum 'a. and
(e:'a. (f:'a hnum 'a. (fn1:hnum 'a. (equal(fn1(0),e)
(e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,all
(e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. equal
(e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. (fn1(suc(n))
(e:'a. (f:'a hnum 'a. (fn1:hnum 'a. ,(n:hnum. ,f(fn1(n),n)))))))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
