the_w:World, l:IdLnk, e:E. sends(l;e) 
Msg_sub(l; the_w.M) ListT:Type, P:(T
), l:T List. filter(P;l) {x:T| P(x) } Lista,b:IdLnk. a = b 
a = b| Theorem | Name |
| the_w:World, l:IdLnk, e:E. sends(l;e) Msg_sub(l; the_w.M) List | [better-w-sends-wf] |
| cites the following: | |
| T:Type, P:(T), l:T List. filter(P;l) {x:T| P(x) } List | [filter_type] |
| a,b:IdLnk. a = b a = b | [assert-eq-lnk] |