IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
es-before wf1 1. the_es : ES
2. e : E
3. x:E. (x <loc e) before(x) E List
before(e) E List
By:
RecUnfold `es-before` 0 THEN SplitOnConclITE THEN BackThru 3
THEN
BackThru Thm*the_es:ES, j:E. first(j) (pred(j) <loc j)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x:E. (x <loc e) 
before(x) 
E List
before(e) 
first(j) 
