proposition: Lemma cunion_countable : countable [pred x | `[< exists i, x \in E i >]].
proof: Proof. pose Ci i : countType := HB.pack [psub (E i)] (countable_countMixin (cE i)). pose S := { i : nat & Ci i }; set F := [pred x | _]. have H: forall (x : [psub F]), exists i : nat, val x \in E i. by case=> x /= /asboolP[i] Eix; exists i. have G: forall (x : S), val (tagged x) \in F. by case=> i [x /= Eix]; apply/asboolP; exists i. pose f (x : [psub F]) : S := Tagged (fun i => [psub E i]) (PSubSub (xchooseP (H x))). pose g (x : S) := PSubSub (G x). by have /can_countable: cancel f g by case=> x hx; apply/val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap reals