proposition: Lemma first_in : forall (d : data) (q : queue data), first data q = value data d -> In_queue data d q.
proof: Proof. simple induction q; simpl in |- *. intros H; discriminate H. intros d0 q0; case q0; intros. inversion H0; auto. right; apply H; auto. Qed.
imports: bibli