proposition: Lemma countable_product (X Y:Type) : CountableT X -> CountableT Y -> CountableT (X * Y).
proof: Proof. intros [f] [g]. pose (fg := fun (p:X*Y) => let (x,y):=p in (f x, g y)). destruct countable_nat_product as [h]. exists (fun p:X*Y => h (fg p)). intros [x1 y1] [x2 y2] H2. apply H1 in H2. injection H2 as H3 H4. apply H in H3. apply H0 in H4. now subst. Qed.
imports: FiniteTypes Relation_Definitions ZArith QArith IndexedFamilies InfiniteTypes CSB DecidableDec FunctionalExtensionality ProofIrrelevance DependentTypeChoice ClassicalChoice Arith ArithRing