fact: Definition Ensemble_fold_right {A B} (f : A -> B -> B) (b : B) (S : Ensemble A) : Comp B := fold_right (fun a b => ret (f a b)) (ret b) S.
imports: Coq.Lists.List Coq.Sets.Ensembles Fiat.Computation.Core Fiat.Computation.Notations Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.Ensembles.Cardinal