proposition: Lemma init_copy_diff_site : forall s1 s2 : Site, In_queue Message copy (bm config_init s1 s2) -> s1 <> s2.
proof: Proof. simpl in |- *; contradiction. Qed.
imports: DistributedReferenceCounting.machine0.machine counting