1. the_w : World
2. FairFifo
3. e : E
4. e' : E
5. loc(e) = loc(e')
6. e <c e'  e <loc e'
  e' <c e  e' <loc e

By:	Inst Thm* the_w:World, e,e':E. Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e') [the_w;e';e] THEN ThinTrivial THEN BackThruSomeHyp

None

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