is mentioned by

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]
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]

In prior sections: bool 1 rel 1 sqequal 1 list 1 mb basic mb nat mb list 1 mb list 2 mb structures mb events mb tree mb automata 1 prog 1

Try larger context: GenAutomata