es:ES, e,e':E. [e, e'] 
{ev:E| loc(ev) = loc(e') Id } ListT:Type, L:T List, P:(T
Prop). (xL.P(x)) 
L {x:T| P(x) } Listes:ES, e,e',ev:E. (ev [e, e']) 
e 
ev & ev e' | Rank | Theorem | Name |
| 5 | es:ES, e,e':E. [e, e'] {ev:E| loc(ev) = loc(e') Id } List | [es-interval_wf2] |
| cites the following: | ||
| 1 | T:Type, L:T List, P:(TProp). (xL.P(x)) L {x:T| P(x) } List | [list-set-type2] |
| 4 | es:ES, e,e',ev:E. (ev [e, e']) e ev & ev e' | [member-es-interval] |