proposition: Lemma alt_post_elsewhere : forall (s1 s2 : Site) (m : Message), s1 <> s0 \/ s2 <> owner -> alternate (b0 s0 owner) -> alternate (Post_message Message m b0 s1 s2 s0 owner).
proof: Proof. intros; rewrite post_elsewhere; trivial. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm