proposition: Lemma not_s1_s2 : forall s s1 s2 : Site, s1 <> s2 -> s1 <> s \/ s2 <> s.
proof: Proof. intros. case (eq_site_dec s1 s). intro; rewrite e. rewrite e in H. right; auto. intro. left; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm