IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable es-E equal the_es:ES, e,e':E. Dec(e = e')
By:
Auto THEN RWO Thm*the_es:ES, e,e':E. e = e'e = e' 0
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
the_es:ES, e,e':E. Dec(e = e')
e = e' 0
