the_w:World, e,e':E. e = e'  e = e'

By:	Auto THENL [BackThru Thm* the_w:World, e,e':E. e = e'  e = e';RevHypSubst -1 0] THEN All Thin

1

1. the_w : World 2. e : E   e = e

1 step

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