(3steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-outlinks-join 1
1. A : MsgAForm
2. B : MsgAForm
3. ltg : IdLnkIdType
4. i : Id
  (ltg  ma-outlinks(A  B;i))
  
  (ltg  ma-outlinks(A;i))  (ltg  ma-outlinks(B;i))
By: RepeatFor 8 (Analyze -4) THEN RepeatFor 8 (Analyze -3)
THEN
Repeat (Unfolds [`ma-outlinks`;`ma-join`;`mk-ma`] 0 THEN Reduce 0)

Generated subgoal:

1 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))
1 step

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

(3steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc