proposition: Lemma countable_bij_fun : Countable A -> Countable B.
proof: Proof. intros H. apply surj_countable with (f := fun_restr (fun_bijection_codomain g_bij)); auto. apply fun_bijection_is_ZL_bijection. Qed.
imports: Coq(Ensembles Arith ArithRing Wellfounded Relations Wf_nat Finite_sets Logic.Epsilon Sets.Image Lia) ZornsLemma(Classical_Wf CountableTypes Families) hydras(MoreEpsilonIota PartialFun GRelations Prelude.More_Arith)