proposition: Lemma sigma_fin_eq_compat : forall (f g : A -> U)(P:A->Prop)(FP:finite P), (forall x, P x -> (f x)==(g x))-> sigma_fin f FP == sigma_fin g FP.
proof: Proof. intros; apply Ole_antisym; apply sigma_fin_monotonic; auto. intros; rewrite (H x); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)