proposition: Lemma alt_post_any : forall m : Message, (forall s : Site, m <> inc_dec s) -> alternate (b0 s0 owner) -> alternate (Post_message Message m b0 s0 owner s0 owner).
proof: Proof. intros; rewrite post_here; apply alt_any_alt; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm