Def (x  l) == i:. i<||l|| & x = l[i]  T

is mentioned by

Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. Thm* (ltg  da-outlinks(da1  da2;i)) Thm*  Thm* (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))	[da-outlinks-join]
Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. Thm* (ltg  da-outlinks(k : T;i)) Thm*  Thm* isrcv(k) & source(lnk(k)) = i Thm* & (1of(ltg) ~ lnk(k)) Thm* & (1of(2of(ltg)) ~ tag(k)) Thm* & 2of(2of(ltg)) = T	[da-outlinks-single]

In prior sections: mb list 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 4

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