At: no DASH dup DASH fusion 1
1. E: TaggedEventStruct
2. P: (|E| List)
Prop
3. I: (|E| List)Prop
4. P refines (Causal(E) 
No-dup-deliver(E))
5. (I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P
P refines Causal(E)
By:
RepeatFor 2 (ParallelOp -2)
THEN
ParallelOp -1
THEN
Unfold `prop_and` -1
THEN
Reduce -1
Generated subgoals:None
About:
