proposition: Lemma permute_sigma_but_reduce : forall q : queue Data, sigma_but Site owner eq_site_dec LS0 (fun s : Site => reduce Data (f s s1 s2) q) = reduce Data (fun d : Data => sigma_but Site owner eq_site_dec LS0 (fun s : Site => f s s1 s2 d)) q.
proof: Proof. elim LS0. simpl in |- *. intro q. rewrite reduce_null_fun. auto. auto. intros a l H q. simpl in |- *. case (eq_site_dec a owner). intro e. auto. intro n. rewrite H. rewrite <- disjoint_reduce. unfold fun_sum in |- *. auto. Qed.
imports: List fifo table reduce