proposition: Lemma countable_countable (T : countType) (E : pred T) : countable E.
proof: Proof. by exists choice.pickle choice.unpickle; apply/choice.pickleK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals