|E| List 
(
Q:(
||L||
Prop). (
i:||L||. Dec(Q(i))) & (i:||L||. Q(i)) & (i:||L||. Q(i) 
(is-send(E)(L[i]))) & (i,j:||L||. Q(i) Q(j) tag(E)(L[i]) = tag(E)(L[j])) & (i,j:||L||. Q(i) i
j C(Q)(j)))
is mentioned
In prior sections: mb hybrid