proposition: Lemma not_in_q_input : forall (data : Set) (d' d : data) (q : queue data), d <> d' -> ~ In_queue data d (input data d' q) -> ~ In_queue data d q.
proof: Proof. intros data0 d' d q H H0. generalize H0. simpl in |- *. intuition. Qed.
imports: bibli