proposition: Lemma Enumerable_Same_set: forall {U} (A B: Ensemble U), Same_set A B -> Enumerable U A -> Enumerable U B.
proof: Proof. intros. destruct X. exists x. destruct a; split; auto. unfold Ensembles.In in *; firstorder. Qed.
imports: Coq.Sorting.Permutation Coq.Classes.EquivDec CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext Coq.Lists.List