proposition: Lemma D_first_out : forall q0 : queue Message, D_queue q0 -> D_queue (first_out Message q0).
proof: Proof. intros; elim H; simpl in |- *. apply D_empty. simple destruct qm. intro. apply D_empty. intros. apply D_dec. apply alt_first_out. auto. Qed.
imports: DistributedReferenceCounting.machine3.machine DistributedReferenceCounting.machine3.cardinal DistributedReferenceCounting.machine3.comm