Nuprl - Proof: w-locl-iff 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-locl-iff 2

1. the_w : World
2. e : E
3. e' : E
4. FairFifo
5. e <loc e'

e <c e'

By:	Unfold `w-causl` 0 THEN Unfold `rel_plus` 0 THEN Reduce 0 THEN InstConcl [1] THEN Repeat (RecUnfold `rel_exp` 0 THEN Reduce 0) THEN InstConcl [e'] THEN OrLeft

Generated subgoals:

None

About:

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