k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm*
f:(tg:Id
State(ds)
ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
Thm*
x
dom(ds). A=ds(x) 
A
Thm*
Thm*
kdom(da). A=da(k) A Feasible(ma-single-sends(ds; da; k; l; f))eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
(x L)