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

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

switchable( < A,f,t > (E))(P o f)
By: Subst ( < A,f,t > (E) = induced_event_str(E;A;f)) 0
Generated subgoals:

1 < A,f,t > (E) = induced_event_str(E;A;f) {E:EventStruct| |E| = A }
2 switchable(induced_event_str(E;A;f))(P o f)
37. z: {E:EventStruct| |E| = A }
switchable(z)(P o f) Prop

About:
listsetapplyfunctionuniverseequalmemberprop

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