proposition: Remark sigma2_change_1 : forall (l : list Site) (n0 : Z), only_once Site eq_site_dec s0 l -> (sigma Site l (change_x0 Site Z eq_site_dec a_fun s0 n0) + a_fun s0 - n0)%Z = sigma Site l a_fun.
proof: Proof. intros l n0 H. rewrite sigma_change. omega. auto. Qed.
imports: List fifo table reduce