Nuprl - Proof: msg-form-join-list

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: msg-form-join-list

L:MsgA List.

(L)

MsgAForm

By:	InductionOnList THEN Unfold `ma-join-list` 0 THEN Reduce 0 THEN Try (Fold `ma-join-list` 0)

Generated subgoals:

1 1. MsgA List
    MsgAForm
1 step

2 1. MsgA List
2. u : MsgA
3. v : MsgA List
4. (v)  MsgAForm
  u  (v)  MsgAForm
3 steps

About:

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

1	1. MsgA List MsgAForm	1 step
2	1. MsgA List 2. u : MsgA 3. v : MsgA List 4. (v) MsgAForm u (v) MsgAForm	3 steps