da:k:Knd fp-> Type, i:Id. da-outlinks(da;i) 
(IdLnk
IdType) ListT:Type, P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List.
Thm* mapfilter(f;P;L)
T' Listi:Id, k:Knd. has-src(i;k) 
isrcv(k) & source(lnk(k)) = i| Rank | Theorem | Name |
| 2 | da:k:Knd fp-> Type, i:Id. da-outlinks(da;i) (IdLnkIdType) List | [da-outlinks_wf] |
| cites the following: | ||
| 1 | T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List.
Thm* mapfilter(f;P;L) T' List | [mapfilter_wf] |
| 0 | i:Id, k:Knd. has-src(i;k) isrcv(k) & source(lnk(k)) = i | [assert-has-src] |