Nuprl - Proof: better-w-sends-wf 1 2 2 1

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

1. the_w : World
2. l : IdLnk
3. e : E
4. v : {m:Msg(the_w.M)| source(mlnk(m)) = loc(e) } List
5. m(loc(e);time(e)) = v
6. v

Msg(the_w.M) List
7. x : Msg(the_w.M)
8. mlnk(x) = l

mlnk(x) = l

By:	RWO Thm* a,b:IdLnk. a = b a = b -1

Generated subgoals:

None

About:

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