Nuprl - Proof: one axiom

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one axiom

'a:S, f,g:('a

Unit). f = g

By:	RewriteOfThm Thm* 'a:S. all(f:'a hone. all(g:'a hone. equal(f,g))) HNC

Generated subgoals:

None

About:

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