At: switchable induced 5
1. E: EventStruct
2. A: Type
3. f: A
|E|
4. P: (|E| List)
Prop
5.
x,y:|E| List. P(x) 
(x asyncR(E) y) 
P(y)
x,y:A List. P(map(f;x)) 
(x asyncR(induced_event_str(E;A;f)) y) 
P(map(f;y))
By:
Auto
THEN
Using [`x',map(f;x);`y',map(f;y)] BackThruSomeHyp
THEN
All (
h.(Unfolds [`induced_event_str`;`R_async`] h) THEN (Reduce h))
THEN
BackThru
Thm*
P:(A
A
Prop), f:(B
A), x,y:B List.
(x swap adjacent[P(f(x),f(y))] y) 
(map(f;x) swap adjacent[P(x,y)] map(f;y))
Generated subgoals:None
About: