L:MsgA List, M:MsgA. (A,B
L.A ||+ B) 
(M L) M 
(L)l:T List, a,x:T. (x [a / l]) 
x = a 
(x l)T:Type{i}, x:T, L:T List, P:(T
TProp{i'}).
Thm* (
x,y[x / L].P(x,y)) (x,yL.P(x,y)) & (yL.P(x,y))M1,M2:MsgA. M1 M1 M2M1,M2,M3:MsgA. M1 M2 M2 M3 M1 M3M1,M2:MsgA. M1 || M2 M2 M1 M2L:MsgA List.
Thm* (
A,BL.A ||+ B) (L) MsgA & (M:MsgA. (BL.M ||+ B) M ||+ (L))