proposition: Lemma sigma_but_simpl : forall (l : list E) (f g : E -> Z), (forall x : E, x <> x0 -> In x l -> f x = g x) -> sigma_but l f = sigma_but l g.
proof: Proof. simple induction l. auto. simpl in |- *; intros. case (eq_E_dec a x0). intro e. apply (H f0 g). intros x H1 H2. apply H0. auto. right; auto. intro n. rewrite H0. rewrite (H f0 g). auto. intros x H1 H2. apply H0. auto. right; auto. auto. left; auto. Qed.
imports: List bibli