(3steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: not rcv locl
  a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a)  False
By: Unfolds [`Knd`;`locl`] 0

Generated subgoals:

1 1. a : Id
2. l : IdLnk
3. tg : Id
4. rcv(l; tg) = inr(a)  (IdLnkId)+Id
  False
1 step
2 1. Id
2. l : IdLnk
3. tg : Id
  rcv(l; tg)  (IdLnkId)+Id
1 step

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

(3steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc