proposition: Lemma reduce_append_nil2 : forall (q1 : queue E) (d : E), reduce (append E q1 (input E d (empty E))) = (reduce q1 + f d)%Z.
proof: Proof. intros q1 d. pattern q1 at 2 in |- *. rewrite <- (append_nil2 E q1). apply reduce_append. Qed.
imports: Bool fifo