proposition: Lemma reduce_simpl : forall (f1 f2 : E -> Z) (q : queue E), (forall d : E, f1 d = f2 d) -> reduce E f1 q = reduce E f2 q.
proof: Proof. simple induction q. simpl in |- *; auto. intros d q0 H H0. simpl in |- *. rewrite H. rewrite H0. auto. auto. Qed.
imports: Bool fifo