1. ltg : IdLnkIdType
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)  [not for witness]
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)
  (ltg  mapfilter(k.da-outlink-f(da2;k);k.has-src(i;k);fpf-dom-list(da2)))

1	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)  IdLnkIdType 15. y  dom(da1  da2) 16. y  dom(da1)   y  {k:Knd| k  dom(da2) }	2 steps
2	(y  fpf-dom-list(da2))	4 steps
3	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)  IdLnkIdType 15. y  dom(da1  da2) 16. y  dom(da1)   ltg = da-outlink-f(da2;y)  IdLnkIdType	4 steps
4	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)  IdLnkIdType 15. y  dom(da1  da2) 16. y  dom(da1) 17. y1 : {k:Knd| k  dom(da2) } 18. has-src(i;y1)   y1  {k:Knd| k  dom(da2) & isrcv(k) }	1 step

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