proposition: Lemma reduce_in_queue_null : forall q : queue E, (forall x : E, In_queue E x q -> f x = 0%Z) -> reduce E f q = 0%Z.
proof: Proof. simple induction q; simpl in |- *. auto. intros d q0 H H0. rewrite H0. rewrite H. auto. intros x H1. apply H0. right; auto. left; auto. Qed.
imports: Bool fifo