(17steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-outlinks-join-list
  L:MsgA List, P:(IdLnkIdTypeProp), i:Id.
  (ML.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks((L);i).P(ltg))
By: InductionOnList THEN Unfold `ma-join-list` 0 THEN Reduce 0
THEN
Try (Fold `ma-join-list` 0)

Generated subgoals:

1 1. MsgA List
  P:(IdLnkIdTypeProp), i:Id.
  (Mnil.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks(;i).P(ltg))
1 step
2 1. MsgA List
2. u : MsgA
3. v : MsgA List
4. P:(IdLnkIdTypeProp), i:Id.
4. (Mv.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks((v);i).P(ltg))
  P:(IdLnkIdTypeProp), i:Id.
  (M[u / v].(ltgma-outlinks(M;i).P(ltg)))
  
  (ltgma-outlinks(u  (v);i).P(ltg))
15 steps

About:
productlistconsnilfunctionuniversepropimpliesall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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