proposition: Lemma FiniteT_nat_cardinal_False: FiniteT_nat_cardinal False empty_finite = 0.
proof: Proof. apply FiniteT_nat_cardinal_cond. rewrite (False_Ensembles_eq _ Empty_set). constructor. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)