proposition: Lemma finite_countable : finite E -> countable E.
proof: Proof. case=> s uqs Es; pose t := pmap (fun x => (insub x : option [psub E])) s. pose f x := index x t; pose g i := nth None [seq Some x | x <- t] i. apply (@Countable _ E f g) => x; rewrite {}/f {}/g /=. have x_in_t: x \in t; first case: x => x h. by rewrite {}/t mem_pmap_sub /= Es. by rewrite (nth_map x) ?index_mem ?nth_index. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals