proposition: Lemma sigma_nowhere : forall l : list E, ~ In x0 l -> sigma E l (change_x0 E Z eq_E_dec f x0 y0) = sigma E l f.
proof: Proof. intros; apply sigma_simpl. intros; apply elsewhere. apply sym_not_eq; apply in_not_in with (l := l); auto. Qed.
imports: List finite