PrintForm Definitions Lemmas hol one Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one axiom 2

  'a:S, e:'a.
  (fn:(Unit'a). fn() = e)
  & (fn,y:(Unit'a). fn() = e & y() = e  fn = y)


By: RewriteOfThm
Thm* 'a:S. all(e:'a. exists_unique(fn:hone  'a. equal(fn(one_el),e)))
HNC


Generated subgoals:

None

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

PrintForm Definitions Lemmas hol one Sections HOLlib Doc