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: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)