At: R async symmetric
E:EventStruct, x,y:|E| List. (x asyncR(E) y) 
(y asyncR(E) x)
By:
Fold `sym` 0
THEN
Unfold `R_async` 0
THEN
BackThru
Thm* P:(A
AProp).
Sym x,y:A. P(x,y) Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2
THEN
Unfold `sym` 0
THEN
Try (ParallelOp -2)
THEN
Try (ParallelOp -1)
Generated subgoals:None
About:
