proposition: Lemma FiniteT_impl_CountableT (X : Type) : FiniteT X -> CountableT X.
proof: Proof. intros. induction H. - exists (False_rect nat). now intro. - destruct IHFiniteT as [f]. exists (fun x => match x with | Some x0 => S (f x0) | None => 0 end). intros [x1|] [x2|] H1; injection H1 as H1 + discriminate H1 + trivial. now destruct (H0 _ _ H1). - destruct IHFiniteT as [g], H0 as [finv]. exists (fun y:Y => g (finv y)). intros y1 y2 ?. apply H1 in H3. congruence. 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)