Nuprl - Proof: bequal refl simp

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bequal refl simp

'a:S, x:'a. (x =

x) = true

By:	Simpsetp [`bequal`;`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