proposition: Lemma cardinal_first_out : forall (q : queue Message) (m : Message), first Message q = value Message m -> cardinal (first_out Message q) = (cardinal q - cardinal_count m)%Z.
proof: Proof. intros. unfold cardinal in |- *. apply reduce_first_out. auto. Qed.
imports: reduce DistributedReferenceCounting.machine2.machine