proposition: Lemma retract_fin_inv : forall (P:A->Prop) (f:A->U), retract_fin P f -> forall Q (FQ: finite Q), incl Q P -> forall x, ~(Q x) -> (P x) -> sigma_fin f FQ <=[1-]f x.
proof: Proof. intros; apply Uinv_le_perm_right; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)