fact: Definition cardinal {A} (ls : list A) : Comp nat := Pick (cardinal _ (elements ls)).
imports: Coq.Lists.List Coq.Sets.Ensembles Fiat.Computation.Core Fiat.Computation.Notations Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.Ensembles.Cardinal