IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
d-realizes2 wf1 1. D : Dsys
2. {es:ES| es is an event system of D }Prop
3. w : World
4. p : FairFifo
5. PossibleWorld(D;w)
ES(w;p) {es:ES| es is an event system of D }
By:
Analyze THEN Unfold `d-es` 0 THEN InstConcl [w;p]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
ES(w;p) 
{es:ES| es is an event system of D }
