At: P no dup iff2 1. E: EventStruct 2. tr: |E| List 3. x,y:|E|.
is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr)
No-dup-deliver(E)(tr) By: ((Unfold `P_no_dup` 0) THEN (Reduce 0) THEN SupposeNot THEN (Decide (i < j)))
THENL
[InstHyp [tr[i];tr[j]] 3;InstHyp [tr[j];tr[i]] 3]
THEN
Try
((Inst
Thm*E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)
[E])
THEN
(Complete UseEquiv))
THEN
Try ((Analyze -1) THEN Easy) Generated subgoals:
x,y:|E|.
is-send(E)(x) 
No-dup-deliver(E)(tr)