da:k:Knd fp-> Type{i}, i:Id. da-outlinks(da;i)  (IdLnkIdType{i}) List

By:	Auto THEN Unfold `da-outlinks` 0 THEN Inst Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List. Thm* mapfilter(f;P;L)  T' List [lexpr{i'};{k:Knd| k  dom(da) }] THEN BackThru -1 THEN Reduce 0

1

1. da : k:Knd fp-> Type{i} 2. i : Id 3. P:({k:Knd| k  dom(da) }), T':Type{i'}, 3. f:({x:{k:Knd| k  dom(da) }| P(x) }T'), L:{k:Knd| k  dom(da) } List. 3. mapfilter(f;P;L)  T' List 4. k : {x:{k:Knd| k  dom(da) }| has-src(i;x) }   k  {k:Knd| k  dom(da) & isrcv(k) }

1 step

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