proposition: Lemma sigma_simpl : forall (l : list E) (f g : E -> Z), (forall x : E, In x l -> f x = g x) -> sigma l f = sigma l g.
proof: Proof. simple induction l. auto. simpl in |- *; intros. rewrite (H f g). rewrite (H0 a); auto. auto. Qed.
imports: List bibli