proposition: Lemma sigma_sigma_but : forall l : list E, only_once E eq_E_dec x0 l -> sigma E l f = (sigma_but l f + f x0)%Z.
proof: Proof. simple induction l. simpl in |- *; intuition. intros a l0 H H0. case (eq_E_dec a x0). intro; rewrite e; simpl in |- *. rewrite case_eq. rewrite sigma_sigma_but_not_in. omega. generalize H0; simpl in |- *. rewrite e. case (eq_E_dec x0 x0). auto. intuition. intros n. simpl in |- *. rewrite case_ineq. rewrite H. omega. generalize H0; simpl in |- *. case (eq_E_dec x0 a). intros e H1. rewrite e in n. elim n. auto. intro n0. auto. auto. Qed.
imports: List bibli