proposition: Lemma not_in_q_input2 : forall (d' d : data) (q : queue data), ~ In_queue data d (input data d' q) -> ~ In_queue data d q.
proof: Proof. simpl in |- *; intros. case (eq_data_dec d d'); intro. elim H; auto. unfold not in |- *; intro; elim H. auto. Qed.
imports: bibli