proposition: Corollary FiniteT_has_nat_cardinal' (X : Type) : FiniteT X -> exists n, cardinal (@Full_set X) n.
proof: Proof. intros. apply FiniteT_dec_Ensemble_has_cardinal; [assumption|]. intros. left. constructor. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)