(8steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: es-loc-rcv
  es:ES, e:E, l:IdLnk, tg:Id.
  kind(e) = rcv(l; tg)  loc(e) = destination(l) & loc(sender(e)) = source(l)
By: Auto THEN Assert isrcv(e)

Generated subgoals:

1 1. es : ES
2. e : E
3. l : IdLnk
4. tg : Id
5. kind(e) = rcv(l; tg)
  isrcv(e)
1 step
2 1. es : ES
2. e : E
3. l : IdLnk
4. tg : Id
5. kind(e) = rcv(l; tg)
6. isrcv(e)
  loc(e) = destination(l) & loc(sender(e)) = source(l)
6 steps

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

(8steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc