Thm* E:EventStruct, P:TraceProperty(E), A:Type, evt:(A |E|)
, tg:(A Label), 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:(A Label)
, 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:EventStruct, A:Type, evt:(A |E|), tg:(A Label), m:Label
, tr1,tr2:A List. (tr1 R(tg) tr2)  < tr1 > _m = < tr2 > _m A List | [tag_sublist_preserved] |
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] |
Def I fuses P == tr:Trace(E). ( m:Label. P( < tr > _m))  I(tr)  P(tr) | [fusion_condition] |