proposition: Lemma sigma2_sigma_but : sigma_but Site s0 eq_site_dec LS0 (fun s : Site => sigma2_table Site LS1 LS2 Data (f s) t) = sigma2_table Site LS1 LS2 Data (fun (s1 s2 : Site) (d : Data) => sigma_but Site s0 eq_site_dec LS0 (fun s : Site => f s s1 s2 d)) t.
proof: Proof. elim LS0. simpl in |- *. unfold sigma2_table in |- *. unfold sigma_table in |- *. rewrite sigma_null. unfold Z_id in |- *. rewrite sigma_null. auto. intros a l H. simpl in |- *. case (eq_site_dec a s0). intro e. auto. intro n. rewrite H. rewrite <- sigma2_disjoint. unfold fun_sum_site2 in |- *. unfold fun_sum_site in |- *. auto. Qed.
imports: List fifo table reduce