is mentioned by

Thm* E:EventStruct, P:TraceProperty(E), A:Type, evt:(A|E|) , tg:(ALabel), tr_u:Trace(E), tr_l:A List. switchable(E)(P) No-dup-send(E)(tr_u) full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u)	[switch_main_theorem]
Thm* E:EventStruct, P:((|E| List)Prop), A:Type, evt:(A|E|), tg:(ALabel) , tr:A List. switchable(E)(P) No-dup-send(E)(map(evt;tr)) switch_inv( < A,evt,tg > (E))(tr) (m:Label. P(map(evt; < tr > _m))) P(map(evt;tr))	[switch_theorem]
Thm* E:TaggedEventStruct, P:TraceProperty(E). switchable(E)(P) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem2]
Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem]
Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) (P refines (Causal(E) No-dup-deliver(E))) (((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P)	[switch_inv_plus_normal]
Thm* E:TaggedEventStruct, tr:Trace(E). (switch_inv(E) No-dup-send(E))(tr) (tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr'))	[switch_normal_exists]
Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E)	[no_duplicate_send_layer]
Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E)	[no_duplicate_send_async]
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E)	[no_duplicate_send_delayable]
Thm* E:TaggedEventStruct. (switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E)) refines single-tag-decomposable(E)	[switch_decomp_implies_single_tag_decomp]
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines (Causal(E) No-dup-deliver(E))) ((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P) ((I No-dup-send(E)) fuses P)	[no_DASH_dup_DASH_fusion]
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines Causal(E)) ((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P)	[tag_by_msg_fusion_lemma]
Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E)	[no_duplicate_send_safety]
Thm* E:TaggedEventStruct, tr:|E| List. (m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr)	[P_tag_by_msg_lemma]
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), tr_l:A List. No-dup-send(E)(map(evt;tr_l)) No-dup-send( < A,evt,tg > (E))(tr_l)	[no_dup_send_induced]

Try larger context: GenAutomata