IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-match-unique221 1. the_w:World, e:E, t,t':.
1. FairFifo
1. 1. isrcv(kind(e))
1. 1. t<t' match(lnk(kind(e));t;time(e)) match(lnk(kind(e));t';time(e))
2. the_w : World
3. e : E
4. t : 5. t' : 6. FairFifo
7. isrcv(kind(e))
8. match(lnk(kind(e));t;time(e))
9. match(lnk(kind(e));t';time(e))
10. t<t' 11. t'<t t = t'
By:
InstHyp [the_w;e;t';t] 1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html