is mentioned by

Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E)

[no_duplicate_send_layer]

In prior sections: mb nat

Try larger context: GenAutomata