proposition: Lemma collect_elsewhere : forall (b0 : Bag_of_message) (s0 s1 s2 s3 : Site), s0 <> s2 \/ s1 <> s3 -> Collect_message b0 s0 s1 s2 s3 = b0 s2 s3.
proof: Proof. intros; unfold Collect_message in |- *; apply other_queue; elim H; auto. Qed.
imports: counting