proposition: Lemma inj_countable {X Y : Type} (f : X -> Y) : CountableT Y -> injective f -> CountableT X.
proof: Proof. intros [g] ?. exists (fun x:X => g (f x)). intros x1 x2 ?. auto. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing