proposition: Lemma surj_countable {X Y : Type} (f : X -> Y) : CountableT X -> surjective f -> CountableT Y.
proof: Proof. intros. destruct (choice (fun (y:Y) (x:X) => f x = y)) as [finv]; trivial. apply inj_countable with finv; trivial. intros x1 x2 ?. congruence. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing