Nuprl - Proof: hi def

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html