proposition: Lemma D_collect : forall s1 s2 : Site, D_queue (b0 s0 owner) -> D_queue (Collect_message b0 s1 s2 s0 owner).
proof: Proof. intros; case (eq_queue_dec s1 s0 s2 owner); intro. decompose [and] a; rewrite H0; rewrite H1. rewrite collect_here; apply D_first_out; trivial. rewrite collect_elsewhere; auto. Qed.
imports: counting