proposition: Lemma equality_from_queue_membership : forall (x y : data) (q : queue data), In_queue data y q -> ~ In_queue data x q -> x <> y.
proof: Proof. simple induction q. simpl in |- *. intuition. intros d q' H. simpl in |- *. case (eq_data_dec y d). intro e. rewrite e. intro H0. intuition. intros n H0 H1. apply H. intuition. intuition. Qed.
imports: bibli