Nuprl - mb_event_system_5 LEMMAs for da_DASH_outlinks_DASH

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

Theorem	Name
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]
cites the following:
Thm* a,x:T. (x [a]) x = a	[member_singleton]
Thm* x:T. (x nil) False	[nil_member]

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