IdType
2. i : Id
3. da1 : k:Knd fp-> Type
4. da2 : k:Knd fp-> Type
5. (ltg
mapfilter(
k.da-outlink-f(da1 
da2;k);k.
5. has-src(i;k);fpf-dom-list(da1
da2)))
6. (ltg
mapfilter(k.da-outlink-f(da1;k);k.has-src(i;k);fpf-dom-list(da1)))
6.
6. (
y:{k:Knd| k dom(da1) }.
6. ((y
fpf-dom-list(da1)) & has-src(i;y) & ltg = da-outlink-f(da1;y))
7. (ltg
mapfilter(k.da-outlink-f(da1;k);k.
7. has-src(i;k);fpf-dom-list(da1)))
(y:{k:Knd| k dom(da1) }.
7. (y
fpf-dom-list(da1)) & has-src(i;y) & ltg = da-outlink-f(da1;y))
8. (ltg
mapfilter(k.da-outlink-f(da2;k);k.has-src(i;k);fpf-dom-list(da2)))
8.
8. (
y:{k:Knd| k dom(da2) }.
8. ((y
fpf-dom-list(da2)) & has-src(i;y) & ltg = da-outlink-f(da2;y))
9. (ltg
mapfilter(k.da-outlink-f(da2;k);k.
9. has-src(i;k);fpf-dom-list(da2)))
(y:{k:Knd| k dom(da2) }.
9. (y
fpf-dom-list(da2)) & has-src(i;y) & ltg = da-outlink-f(da2;y))
10. y : Knd
11. y
dom(da1 da2)
12. (y
fpf-dom-list(da1 da2))
13. has-src(i;y)
14. ltg = da-outlink-f(da1
da2;y)
15. y
dom(da1 da2)
16. y
dom(da1)
mapfilter(k.da-outlink-f(da2;k);k.has-src(i;k);fpf-dom-list(da2))
(IdLnkIdType) List
