L:MsgA List. 
  (A,BL.A ||+ B)  (L)  MsgA & (M:MsgA. (BL.M ||+ B)  M ||+ (L))

1	1. MsgA List   (A,Bnil.A ||+ B)      (nil)  MsgA & (M:MsgA. (Bnil.M ||+ B)  M ||+ (nil))	1 step
2	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]))	5 steps

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