proposition: Lemma countable_exp (X Y : Type) : FiniteT X -> CountableT Y -> CountableT (X -> Y).
proof: Proof. intros. induction H. - exists (fun _ => 0). red; intros. extensionality f. destruct f. - destruct (countable_product (T -> Y) Y) as [f]; trivial. exists (fun g => f (fun x => g (Some x), g None)). intros g1 g2 ?. apply H1 in H2. extensionality o. destruct o; injection H2; trivial. intros. pose proof (equal_f H4). apply H5. - destruct H1 as [f1], IHFiniteT as [f0]. exists (fun h => f0 (fun x => h (f x))). intros h1 h2 ?. apply H3 in H4. pose proof (equal_f H4). simpl in H5. extensionality y. rewrite <- (H2 y). apply H5. 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)