1. da : k:Knd fp-> Type
2. i : Id
3. P:({k:Knd| k  dom(da) }), T':Type,
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) }

By:	DVar `k' THEN DVar `k' THEN RWO Thm* i:Id, k:Knd. has-src(i;k)  isrcv(k) & source(lnk(k)) = i -1 THEN ExRepD

None

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