1. D : Dsys
2. P : {es:ES| es is an event system of D }Prop
3. w:World, p:FairFifo. PossibleWorld(D;w)  P(ES(w))
4. D' : Dsys
5. D  D'
6. w : World
7. FairFifo
8. PossibleWorld(D';w)
  PossibleWorld(D;w)

By:	Inst Thm* A,B:Dsys. A  B  (w:World. PossibleWorld(B;w)  PossibleWorld(A;w)) [D;D';w]

None

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