Nuprl - Proof: w-match-unique 1 1 1 1 2

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

1. the_w : World
2. e : E
3. t :

4. t' :

5. FairFifo
6. isrcv(kind(e))
7. t<t'
8. f :

(Msg List)
9. (

t1.onlnk(lnk(kind(e));m(source(lnk(kind(e)));t1))) = f

||concat(map(f;upto(t)))||+||f(t)||

||concat(map(f;upto(t')))||

By:

Thin -1

Generated subgoal:

1 ||concat(map(f;upto(t)))||+||f(t)||||concat(map(f;upto(t')))||
1 step

About:

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