fact: Definition FilteredList (xs : list A) (P : Ensemble A) := ListComprehension (fun x => List.In x xs /\ P x).
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation