Nuprl - Proof: hi thm

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

'a:S. all(

x:'a. equal(i(x),x))

By:	HOL "hi_thm"

Generated subgoals:

None

About:

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