proposition: Lemma append_first : forall (q1 : queue data) (d : data), first data (append q1 (input data d (empty data))) = value data d.
proof: Proof. intros q1 d. elim q1. simpl in |- *. trivial. intros d0 q H. rewrite <- input_append. unfold first in |- *. rewrite case_append_right. unfold first in H. apply H. Qed.
imports: bibli