proposition: Lemma sigma_table_change_aux : only_once Site eq_site_dec s0 LS -> (sigma_table Site LS Data f (update_table Site eq_site_dec Data t s0 d0) + f s0 (t s0) - f s0 d0)%Z = sigma_table Site LS Data f t.
proof: Proof. intro H. rewrite sigma_table_change. omega. auto. Qed.
imports: List fifo table reduce