D,D':Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
  D realizes es.P(es)  D  D'  D' realizes es.P(es)

By:	Unfold `guard` 0 THEN MoveToHyp -2 -1 THEN RepeatFor 3 (ParallelOp -1) THEN Using [`D2',D'] (BackThru Thm* D1,D2,D3:Dsys. D1  D2  D2  D3  D1  D3)

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html