is mentioned by

Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), m:Label , tr1,tr2:A List. (tr1 R(tg) tr2) < tr1 > _m = < tr2 > _m A List	[tag_sublist_preserved]
Def full_switch_inv(E;A;evt;tg;tr_u;tr_l) == tr_m:A List. (tr_l R(tg) tr_m) & (map(evt;tr_m) layerR(E) tr_u) & switch_inv( < A,evt,tg > (E))(tr_m)	[full_switch_inv]

Try larger context: GenAutomata