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)f:(AB), as:A List. ||map(f;as)|| = ||as|| 
| Theorem | Name |
|
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] |
| cites | |
|
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as|| | [map_length] |