proposition: Lemma D_first_out : forall q0 : queue Message, D_queue q0 -> D_queue (first_out Message q0).
proof: Proof. intros. elim H. simpl in |- *. apply D_empty. simple destruct qm. simpl in |- *. intros. apply D_empty. intros. apply D_dec. apply alt_first_out. auto. apply in_q_before_first_out. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm