Nuprl - Pf switchable_induced

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

< A,f,t > (E) = induced_event_str(E;A;f) {E:EventStruct| |E| = A }

By: Analyze

Generated subgoals:

1 < A,f,t > (E) = induced_event_str(E;A;f) EventStruct

2 | < A,f,t > (E)| = A

About:

1	`< A,f,t > (E) = induced_event_str(E;A;f) EventStruct`
2	`\| < A,f,t > (E)\| = A`