proposition: Lemma countable_image : forall (U V:Type)(DA : Ensemble U)(f:U->V), Countable DA -> Countable (image DA f).
proof: Proof. intros. rewrite image_as_Im. apply countable_img. assumption. 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)