proposition: Lemma different_queue2 : forall (E : Set) (q : queue E) (m : E), first E q = value E m -> q <> first_out E q.
proof: Proof. intro. simple induction q. simpl in |- *; intros; discriminate. intro; intro. case q0. simpl in |- *. intros. discriminate. intros. cut (first_out E (input E d (input E e q1)) = input E d (first_out E (input E e q1))). intro. rewrite H1. injection. generalize H; unfold not in |- *; intro. intro. apply (H3 m). auto. auto. simpl in |- *; auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8