ltg:(IdLnk
IdType), i:Id, da1,da2:k:Knd fp-> Type.
Thm* (ltg
da-outlinks(da1 
da2;i))
Thm*
Thm* (ltg
da-outlinks(da1;i)) 
(ltg da-outlinks(da2;i))P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'.
Thm* (x
mapfilter(f;P;L)) 
(
y:T. (y L) & P(y) & x = f(y))eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L)eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A.
Thm* f
g(x) ~ if x dom(f)
f(x) else g(x) fiB:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x
dom(f g) x dom(f) x dom(g)i:Id, k:Knd. has-src(i;k) isrcv(k) & source(lnk(k)) = i