Nuprl - Proof: better-w-sends-wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: better-w-sends-wf

the_w:World, l:IdLnk, e:E. sends(l;e)

Msg_sub(l; the_w.M) List

By:	Unfold `w-sends` 0 THEN UnivCD THEN Unfolds [`Msg_sub`;`w-onlnk`] 0 THEN Unfold `haslink` 0

Generated subgoal:

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
6 steps

About:

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