is mentioned by

Thm* a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg)  False	[not_locl_rcv]
Thm* a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a)  False	[not_rcv_locl]
Thm* x:A, y:B. inl(x) = inr(y)  A+B  False	[inl_eq_inr]

In prior sections: core bool 1 mb list 1 mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html