(7steps 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-join-list-is-empty
  L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;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
  ma-is-empty() ~ true
1 step
2 1. MsgA List
2. u : MsgA
3. v : MsgA List
4. ma-is-empty((v)) ~ reduce(M,x. ma-is-empty(M)x;true;v)
  ma-is-empty(u  (v)) ~ (ma-is-empty(u)reduce(M,x. ma-is-empty(M)
  x;true;v))
5 steps

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

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