Nuprl - mb_event_system_3 LEMMAs for w_DASH_when

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

Theorem	Name
Thm* the_w:World, x:Id, e:E. (x when e) vartype(loc(e);x)	[w-when_wf]
cites the following:
Thm* the_w:World, i:Id, t:, x:Id. s(i;t).x vartype(i;x)	[w-s_wf]

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