proposition: Lemma FiniteT_nat_cardinal_def: forall (X:Type) (H:FiniteT X), cardinal _ (@Full_set X) (FiniteT_nat_cardinal X H).
proof: Proof. intros; unfold FiniteT_nat_cardinal. destruct constructive_definite_description. assumption. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality