At: switchable induced 3 1 1 1
1. E: EventStruct
2. A: Type
3. f: A
|E|
4. P: (|E| List)Prop
5. 
x,y,z:|E| List. P(x) 
P(y) (x
x.(yy.
(x =msg=(E) y))) & z = (x @ y) P(z)
6. x: A List
7. y: A List
8. z: A List
9. P(map(f;x))
10. P(map(f;y))
11. (x@0x.(y@0y.(x@0 =msg=(induced_event_str(E;A;f)) y@0)))
12. x@0: A
13. (x@0 x) (y@0y.(x@0 =msg=(induced_event_str(E;A;f)) y@0))
(x@0 x) (y@0y.((f(x@0)) =msg=(E) (f(y@0))))
By:
Unfolds [`event_msg_eq`;`induced_event_str`] -1
THEN
Reduce -1
THEN
Unfold `event_msg_eq` 0
THEN
Reduce 0
THEN
Trivial
Generated subgoals:None
About:
