is mentioned by

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]
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]

Try larger context: GenAutomata