Nuprl - Pf no_dup

E:TaggedEventStruct. Tag-by-msg(E) fuses No-dup-deliver(E)

By: Unfold `fusion_condition` 0 THEN Unfold `str_trace` 0 THEN Try (Fold `trace_property` 0)

Generated subgoal:

1 1. E: TaggedEventStruct
2. tr: |E| List
3. m:Label. No-dup-deliver(E)( < tr > _m)
4. Tag-by-msg(E)(tr)
No-dup-deliver(E)(tr)

About: