is mentioned by

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