msg:(A
A
), L1,L2:A List.
(a,b:A. (a 
L1) 
(b L2) 
msg(a,b)) (L1 -msg(a,b) L2) = L1P:(T), L:T List. (xL.P(x)) filter(P;L) = L| Rank | Theorem | Name |
| 2 |
Thm* msg:(AA), L1,L2:A List.
(a,b:A. (a L1) (b L2) msg(a,b)) (L1 -msg(a,b) L2) = L1 | [remove_msgs_disjoint] |
| cites | ||
| 1 |
Thm* P:(T), L:T List. (xL.P(x)) filter(P;L) = L | [filter_trivial2] |