proposition: Lemma sigma__S : forall g : E -> Z, g x0 = (f x0 + 1)%Z -> (forall x : E, x <> x0 -> g x = f x) -> sigma E L g = (sigma E L f + 1)%Z.
proof: Proof. intros; rewrite <- sigma_change_S. apply sigma_simpl. intros; unfold change_x0 in |- *. case (eq_E_dec x0 x); simpl in |- *; intro. rewrite <- e; auto. auto. Qed.
imports: List finite