proposition: Lemma dec_is_not_inc : forall s : Site, dec <> inc_dec s.
proof: Proof. intro; discriminate. Qed.
imports: DistributedReferenceCounting.machine3.machine DistributedReferenceCounting.machine3.cardinal DistributedReferenceCounting.machine3.comm