proposition: Lemma Finite_impl_Countable: forall {X : Type} (S : Ensemble X), Finite S -> Countable S.
proof: Proof. intros. now apply FiniteT_impl_CountableT, Finite_ens_type. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)