proposition: Lemma sigma_fin_unique : forall f P Q (FP:finite P) (FQ:finite Q), (equiv P Q) -> sigma_fin f FP == sigma_fin f FQ.
proof: Proof. intros; apply Ole_antisym. apply sigma_fin_incl; auto. apply sigma_fin_incl; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)