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

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

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

onlnk(lnk(kind(e));m(source(lnk(kind(e)));t)) = f(t)

Msg List

By:	RevHypSubst -1 0 THEN Reduce 0 THEN Unfold `w-Msg` 0

Generated subgoals:

None

About:

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