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. apply alt_any_alt. intro; discriminate. auto. simpl in |- *. case (eq_bool_dec false); intro. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm