(9steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switchable induced tagged 1 2
1. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. f: A|E|
5. t: ALabel
6. switchable(E)(P)

switchable(induced_event_str(E;A;f))(P o f)
By: BackThru 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)
Generated subgoals:

None

About:
listapplyfunctionuniverseprop

(9steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc