proposition: Lemma countable_sum (X Y : Type) : CountableT X -> CountableT Y -> CountableT (X + Y).
proof: Proof. intros [f] [g]. destruct countable_nat_product as [h]. exists (fun s:X+Y => match s with | inl x => h (0, f x) | inr y => h (1, g y) end). intros [x1|y1] [x2|y2] ?; apply H1 in H2; try discriminate H2; intros; f_equal; apply H + apply H0; now injection H2. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing