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