proposition: Corollary FiniteT_Finite X (U : Ensemble X) : FiniteT X -> Finite U.
proof: Proof. intros. apply FiniteT_dec_Finite; try assumption. intros. apply classic. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)