es:ES, i:Id, P:({e:E| loc(e) = i 
Id }
Prop).
Thm*
e@i.P(e) 
e@i.first(e) 
P(e) & e@i.
first(e) P(pred(e)) P(e)the_es:ES, e:E. first(e) loc(pred(e)) = loc(e) Id| Theorem | Name |
| es:ES, i:Id, P:({e:E| loc(e) = i Id }Prop).
Thm* e@i.P(e) e@i.first(e) P(e) & e@i.first(e) P(pred(e)) P(e) | [alle-at-iff] |
| cites the following: | |
| the_es:ES, e:E. first(e) loc(pred(e)) = loc(e) Id | [es-loc-pred] |