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