the_w:World, x:Id, e:E. (x when e)  vartype(loc(e);x)

By:	Auto THEN Inst Thm* the_w:World, i:Id, t:, x:Id. s(i;t).x  vartype(i;x) [the_w;loc(e);time(e);x] THEN NthHypSq -1 THEN Analyze THEN Try Trivial

1

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

1 step

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