proposition: Lemma not_D_queue : forall (q0 : queue Message) (m : Message), m <> dec -> ~ D_queue (input Message m q0).
proof: Proof. intros; red in |- *; intro. inversion H0. elim H; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm