is mentioned by

Thm* E:EventStruct, P:TraceProperty(E), L,L1:|E| List. memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1))	[memoryless_remove_msgs]
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]

Try larger context: GenAutomata