(5steps 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-feasible
  L:MsgA List. (A,BL.A ||+ B)  (AL.Feasible(A))  Feasible((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
  (A,Bnil.A ||+ B)  (Anil.Feasible(A))  Feasible()
1 step
2 1. MsgA List
2. u : MsgA
3. v : MsgA List
4. (A,Bv.A ||+ B)  (Av.Feasible(A))  Feasible((v))
  (A,B[u / v].A ||+ B)  (A[u / v].Feasible(A))  Feasible(u  (v))
3 steps

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

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