IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hone axiom 2 'a:S. all(e:'a. exists_unique(fn:hone 'a. equal(fn(one_el),e)))
By:
HOL "hone_axiom_2"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a:S. all(
e:'a. exists_unique(
'a. equal(fn(one_el),e)))
