fact: Definition build_FilteredList (xs : list A) (P : Ensemble A) : Comp (list A) := fold_right (fun (a : A) (l : Comp (list A)) => l' <- l; b <- { b | decides b (P a) }; if b then ret (a :: l') else ret l' ) (ret nil) xs.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation