msg:(A
A
), L1,L2:A List.
(x:A. (x 
L1) 
(x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nilP:(T), L:T List. (xL.
P(x)) (filter(P;L) ~ nil)| Theorem | Name |
|
Thm* msg:(AA), L1,L2:A List.
(x:A. (x L1) (x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nil | [remove_msgs_nil] |
| cites | |
|
Thm* P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ nil) | [filter_is_nil] |