A,B,T:Type, x:Id, a:Knd, tg:Id, l:IdLnk, f:(A
B(T List)).
Thm* (a = rcv(l; tg)
T = B)
Thm*
Thm* ma-single-sends1(A; B; T; x; a; l; tg; f)
MsgAeq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
Thm* f
g(x)?z ~ if x dom(f)
f(x)?z else g(x)?z fid:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
eq:EqDecider(A), x,y:A, v:Top. x dom(y : v) 
x = y