proposition: Lemma sigma_fin_rem : forall f P (FP:finite P) a, P a -> sigma_fin f FP == f a + sigma_fin f (finite_rem decA a FP).
proof: Proof. induction FP; intuition. case (equiv_empty_false a e);auto. simpl; case (decA x a); simpl; intros. case e0; unfold eq_rect_r;simpl; auto. rewrite sigma_fin_equiv; auto. rewrite (IHFP a); auto. case (e a); unfold add; intuition. case f0; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)