proposition: Lemma in_collect : forall (m : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site), In_queue Message m (Collect_message bom s1 s2 s3 s4) -> In_queue Message m (bom s3 s4).
proof: Proof. intros m bom s1 s2 s3 s4; case (eq_queue_dec s1 s3 s2 s4); intro. decompose [and] a; rewrite H; rewrite H0. rewrite collect_here; intros; apply in_q_output; trivial. rewrite collect_elsewhere; auto. Qed.
imports: counting