the_w:World, e:E. first(e)  pred(e)  E

By:	Auto THEN Inst Thm* the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E [the_w;time(e);loc(e)] THEN All (RWO Thm* the_w:World, e:E. <loc(e),time(e)> ~ e)

None

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