IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
es-loc-rcv21 1. es : ES
2. e : E
3. l : IdLnk
4. tg : Id
5. kind(e) = rcv(l; tg)
6. isrcv(e)
7. loc(e) = destination(l)
loc(e) = destination(l)
By:
Inst_ES_Axiom [e] 13 THEN Unfold `es-lnk` -1 THEN HypSubst' -4 -1
THEN
Unfolds [`lnk`;`rcv`] -1
THEN
Reduce -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
loc(e) = destination(l)
loc(e) = destination(l)
