proposition: Lemma D_post_dec : alternate (b0 s0 owner) -> D_queue (Post_message Message dec b0 s0 owner s0 owner).
proof: Proof. intros; rewrite post_here; apply D_dec; auto. Qed.
imports: DistributedReferenceCounting.machine3.machine DistributedReferenceCounting.machine3.cardinal DistributedReferenceCounting.machine3.comm