proposition: Lemma reduce_null_fun : forall q : queue E, (forall d : E, f d = 0%Z) -> reduce q = 0%Z.
proof: Proof. intro; elim q. intro; apply reduce_nil. intros; simpl in |- *. rewrite H. rewrite H0. auto. auto. Qed.
imports: Bool fifo