proposition: Lemma in_q_before_append2 : forall q1 q2 : queue Message, In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) -> In_queue_before Message dec is_inc_dec (append Message q1 q2).
proof: Proof. simple induction q1; simpl in |- *. intros. elim H; intro. discriminate. auto. intro. case d. simpl in |- *. intros. auto. intro. simpl in |- *. auto. simpl in |- *. intros. right. elim H0; intro. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm