PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-first wf
  the_w:World, e:E. first(e)  
By: Auto THEN Analyze -1 THEN Analyze -2
THEN
BackThru Thm* the_w:World, i:Id, t:. first(<i,t>)  

Generated subgoals:

None

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

PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc