1. x:Id fp-> Top
2. A3 : x:Knd fp-> Type
3. x:Id fp-> Top
4. x:Id fp-> Top
5. x:KndId fp-> Top
6. x:KndIdLnk fp-> Top
7. x:Id fp-> Top
8. x:IdLnkId fp-> Top
9. Top
10. x:Id fp-> Top
11. B3 : x:Knd fp-> Type
12. x:Id fp-> Top
13. x:Id fp-> Top
14. x:KndId fp-> Top
15. x:KndIdLnk fp-> Top
16. x:Id fp-> Top
17. x:IdLnkId fp-> Top
18. Top
19. ltg : IdLnkIdType
20. i : Id
  (ltg  da-outlinks(A3  B3;i))
  
  (ltg  da-outlinks(A3;i))  (ltg  da-outlinks(B3;i))

By:	Auto THEN BackThru Thm* ltg:(IdLnkIdType), 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))

None

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