proposition: Lemma countable_union2 {X : Type} {U V : Ensemble X} : Countable U -> Countable V -> Countable (Union U V).
proof: Proof. intros HU HV. assert (exists h : {x : X | In (Union U V) x} -> {x : X | In U x} + {x : X | In V x}, injective h) as [h Hh]. 2: { apply inj_countable with (f := h); auto. apply countable_sum; assumption. } unshelve eexists (fun p : { x : X | In (Union U V) x } => match (classic_dec (In U (proj1_sig p))) with | left Hl => inl (exist U (proj1_sig p) Hl) | right Hr => match (classic_dec (In V (proj1_sig p))) with | left Hl => inr (exist V (proj1_sig p) Hl) | right Hr0 => False_rect _ _ end end). { destruct (proj2_sig p); auto. } simpl in *. intros [x0 Hx0] [x1 Hx1] Hx. simpl in *. repeat (try discriminate; try (inversion Hx0; subst; contradiction); try (inversion Hx1; subst; contradiction); destruct (classic_dec _)). all: inversion Hx; subst; clear Hx; destruct (proof_irrelevance _ Hx0 Hx1); reflexivity. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)