is mentioned by

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: rel 1

Try larger context: GenAutomata