IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-when wf1 1. the_w : World
2. x : Id
3. e : E
4. s(loc(e);time(e)).x vartype(loc(e);x)
(x when e) ~ s(loc(e);time(e)).x
By:
Unfolds [`w-when`;`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 when e) ~ s(loc(e);time(e)).x
