E:TaggedEventStruct. switch_inv(E) 
(|E| List)
PropE:TaggedEventStruct. E EventStruct| Theorem | Name |
|
Thm* E:TaggedEventStruct. switch_inv(E) (|E| List)Prop | [switch_inv_wf] |
| cites | |
| Thm* E:TaggedEventStruct. E EventStruct | [tagged_event_str_subtype] |