IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-after wf1 1. the_w : World
2. x : Id
3. e : E
4. s(loc(e);time(e)+1).x vartype(loc(e);x)
(x after e) ~ s(loc(e);time(e)+1).x
By:
Unfolds [`w-after`;`w-loc`;`w-time`] 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
vartype(loc(e);x)
(x after e) ~ s(loc(e);time(e)+1).x
