proposition: Corollary countable_singleton {X : Type} (x : X) : Countable (Singleton x).
proof: Proof. apply Finite_impl_Countable. apply Singleton_is_finite. 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)