proposition: Corollary FiniteT_dec_Finite X (U : Ensemble X) : FiniteT X -> (forall x : X, In U x \/ ~ In U x) -> Finite U.
proof: Proof. intros. apply FiniteT_dec_Ensemble_has_cardinal in H0; try assumption. destruct H0 as [n]. apply cardinal_finite with (n := n). assumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)