E:EventStruct, P:((|E| List)
Prop), A:Type, f:(A|E|)
, t:(ALabel). switchable(E)(P) 
switchable( < A,f,t > (E))(P o f)E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop).
switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f)| Rank | Theorem | Name |
| 3 |
Thm* E:EventStruct, P:((|E| List)Prop), A:Type, f:(A|E|)
, t:(ALabel). switchable(E)(P) switchable( < A,f,t > (E))(P o f) | [switchable_induced_tagged] |
| cites | ||
| 2 |
Thm* E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop).
switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f) | [switchable_induced] |