proposition: Lemma sigma_change : forall l : list E, only_once E eq_E_dec x0 l -> sigma E l (change_x0 E Z eq_E_dec f x0 y0) = (sigma E l f - f x0 + y0)%Z.
proof: Proof. simple induction l; simpl in |- *. contradiction. intros a l0 hrec; case (eq_E_dec x0 a); intros. rewrite <- e; rewrite here. rewrite sigma_nowhere. omega. trivial. rewrite elsewhere. rewrite hrec. omega. trivial. trivial. Qed.
imports: List finite