fact: Definition ListComprehension (P : Ensemble A) := {l | forall x, List.In x l <-> P x }.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation