fact: Definition FiniteT_nat_cardinal (X:Type) (H:FiniteT X) : nat := proj1_sig (constructive_definite_description _ (FiniteT_has_nat_cardinal X H)).
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality