proposition: Lemma alt_collect : forall s1 s2 : Site, alternate (b0 s0 owner) -> alternate (Collect_message 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 alt_first_out; trivial. rewrite collect_elsewhere; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm