At: switch main theorem 2 1
1. E: EventStruct
2. P: (|E| List)
Prop
3. A: Type
4. evt: A|E|
5. tg: ALabel
6. tr_u: |E| List
7. tr_l: A List
8. switchable(E)(P)
9. No-dup-send(E)(tr_u)
10. tr_m: A List
11. tr_l R(tg) tr_m
12. map(evt;tr_m) layerR(E) tr_u
13. switch_inv( < A,evt,tg > (E))(tr_m)
14. 
m:Label. P(map(evt; < tr_l > _m))
15. m: Label
< tr_m > _m = < tr_l > _m 
A List
By:
Symmetry
THEN
BackThru
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
Generated subgoals:None
About:
