PrintForm Definitions Lemmas hol one Sections HOLlib Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one wd
  v:Unit. v = 
By: RewriteOfThm Thm* all(v:hone. equal(v,one_el)) HNC

Generated subgoals:

None

About:
assertunititapplyequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas hol one Sections HOLlib Search Doc