1. MsgA List
2. u : MsgA
3. v : MsgA List
4. (A,Bv.A ||+ B)  (v)  MsgA & (M:MsgA. (Bv.M ||+ B)  M ||+ (v))
  (A,B[u / v].A ||+ B)
  
  ([u / v])  MsgA & (M:MsgA. (B[u / v].M ||+ B)  M ||+ ([u / v]))

By:	Analyze 0 THEN RWO Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y)) -1 THEN ThinTrivial THEN Unfolds [`ma-join-list`] 0 THEN Reduce 0 THEN Fold `ma-join-list` 0

1	4. (A,Bv.A ||+ B) 5. (Bv.u ||+ B) 6. (v)  MsgA 7. M:MsgA. (Bv.M ||+ B)  M ||+ (v)   u ||decl (v)	3 steps
2	4. (A,Bv.A ||+ B) 5. (Bv.u ||+ B) 6. M : MsgA 7. (B[u / v].M ||+ B) 8. (v)  MsgA 9. M:MsgA. (Bv.M ||+ B)  M ||+ (v)   M ||+ u  (v)	1 step

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