Nuprl - Proof: hi def

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

'a:S. equal(i,s(k,k))

By:	Simpsetp [`hol_to_nuprl`] THEN StrongAuto

Generated subgoals:

None

About:

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