IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-locl-iff3 1. the_w : World
2. e : E
3. e' : E
4. FairFifo
5. loc(e) = loc(e')
6. e <c e' e <loc e'
By:
Unfold `w-locl` 0
THEN
BackThru Thm*the_w:World, e,e':E. FairFifo e <c e' time(e)<time(e')
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
e <loc e'
the_w:World, e,e':E. FairFifo 
e <c e' 
