proposition: Lemma append_first_out2 : forall (d : data) (q1 : queue data), first data q1 = value data d -> append (first_out data q1) (input data d (empty data)) = q1.
proof: Proof. intro; intro. elim q1. simpl in |- *. intuition. discriminate. intros d0 q0. case q0. intros H H0. simpl in |- *. unfold first in H0. inversion H0. trivial. intros d1 q H H0. rewrite first_out_input. rewrite <- input_append. rewrite H. auto. rewrite <- (first_input d0 d1 q). auto. Qed.
imports: bibli