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