(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-sub-join-list
  L:MsgA List, M:MsgA. (A,BL.A ||+ B)  (M  L)  M  (L)
By: InductionOnList THEN Unfold `ma-join-list` 0 THEN Reduce 0
THEN
Try (Fold `ma-join-list` 0)

Generated subgoals:

1 1. MsgA List
  M:MsgA. (A,Bnil.A ||+ B)  (M  nil)  M  
1 step
2 1. MsgA List
2. u : MsgA
3. v : MsgA List
4. M:MsgA. (A,Bv.A ||+ B)  (M  v)  M  (v)
  M:MsgA. (A,B[u / v].A ||+ B)  (M  [u / v])  M  u  (v)
15 steps

About:
listconsnilimpliesall
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