Rank | Theorem | Name |
2 | Thm* da:k:Knd fp-> Type, i:Id. da-outlinks(da;i) (IdLnk Id Type) List | [da-outlinks_wf] |
cites the following: |
1 | Thm* 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 | Thm* i:Id, k:Knd. has-src(i;k)  isrcv(k) & source(lnk(k)) = i | [assert-has-src] |