proposition: Lemma Union_is_Countable_Union: forall {U: Type} (A B: Ensemble U), Same_set (Union _ A B) (Countable_Union _ (Binart_set_list _ A B)).
proof: Proof. intros. rewrite Same_set_spec. intros x. rewrite Union_spec; unfold Countable_Union. split. + intros [? | ?]. - exists 0; auto. - exists 1; auto. + intros [[ | [ | ]] ?]. - left; auto. - right; auto. - intros; inversion H. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext