the_es:ES, e,e':E.
Thm* (e <loc e')
first(e') & e = pred(e') 
E 
(e <loc pred(e'))the_es:ES, e:E. first(e) 
loc(pred(e)) = loc(e) Id| Theorem | Name |
| the_es:ES, e,e':E.
Thm* (e <loc e') first(e') & e = pred(e') E (e <loc pred(e')) | [es-locl-iff] |
| cites the following: | |
| the_es:ES, e:E. first(e) loc(pred(e)) = loc(e) Id | [es-loc-pred] |