proposition: Lemma collect_here : forall (b0 : Bag_of_message) (s0 s1 : Site), Collect_message b0 s0 s1 s0 s1 = first_out Message (b0 s0 s1).
proof: Proof. intros; unfold Collect_message in |- *; apply that_queue. Qed.
imports: counting