fact: Definition elements {A} (ls : list A) : Ensemble A := fun x => List.In x ls.
imports: Coq.Lists.List Coq.Sets.Ensembles Fiat.Computation.Core Fiat.Computation.Notations Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.Ensembles.Cardinal