proposition: Lemma D_input : forall q : queue Message, D_queue (input Message copy q) -> D_queue q.
proof: Proof. intros. inversion H. inversion H0. apply D_dec. auto. generalize H1; simpl in |- *. case (eq_bool_dec false); intro. discriminate. intro. elim H7; intro. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm