es:ES, e,e':E. [e, e']  {ev:E| loc(ev) = loc(e')  Id } List

By:	Auto THEN BackThru Thm* T:Type, L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List

1

1. es : ES 2. e : E 3. e' : E   (ev[e, e'].loc(ev) = loc(e')  Id)

2 steps

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