Nuprl - Pf P_no_dup_deliver

E:EventStruct. safetyR(E) preserves No-dup-deliver(E)

By: Auto THEN BackThru Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P safetyR(E) preserves P

Generated subgoals:

1 1. E: EventStruct
No-dup-deliver(E) TraceProperty(E)

2 1. E: EventStruct
R_strong_safety(E) preserves No-dup-deliver(E)

About:

1	1. `E:` `EventStruct` `No-dup-deliver(E) TraceProperty(E)`
2	1. `E:` `EventStruct` `R_strong_safety(E) preserves No-dup-deliver(E)`