(7steps total) 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: better-w-sends-wf 1
1. the_w : World
2. l : IdLnk
3. e : E
  filter(ms.mlnk(ms) = l;m(loc(e);time(e)))
   {m:Msg(the_w.M)| mlnk(m) = l } List
By: GenConclAtAddr [2;2] THEN Assert (v  Msg(the_w.M) List)

Generated subgoals:

1 4. v : {m:Msg(the_w.M)| source(mlnk(m)) = loc(e) } List
5. m(loc(e);time(e)) = v  {m:Msg(the_w.M)| source(mlnk(m)) = loc(e) } List
  v  Msg(the_w.M) List
Auto
2 4. v : {m:Msg(the_w.M)| source(mlnk(m)) = loc(e) } List
5. m(loc(e);time(e)) = v  {m:Msg(the_w.M)| source(mlnk(m)) = loc(e) } List
6. v  Msg(the_w.M) List
  filter(ms.mlnk(ms) = l;v)  {m:Msg(the_w.M)| mlnk(m) = l } List
4 steps

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

(7steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc