proposition: Corollary countable_empty {X : Type} : Countable (@Empty_set X).
proof: Proof. apply Finite_impl_Countable. apply Empty_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)