proposition: Lemma D_queue_is_alternate : forall q0 : queue Message, D_queue q0 -> alternate q0.
proof: Proof. intros. elim H. apply alt_null. intros. apply alt_any_alt. intro; discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine3.machine DistributedReferenceCounting.machine3.cardinal DistributedReferenceCounting.machine3.comm