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: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing