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) EventStruct

By: Unfolds [`induced_tagged_event_str`;`induced_event_str`;`event_str`] 0

Generated subgoal:

1 < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f,t, > = < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f, > E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top

About: