proposition: Lemma Enumerable_is_EnumCovered: forall U A, Enumerable U A -> EnumCovered U A.
proof: Proof. intros. destruct X as [l [? ?]]. exists l. firstorder. Qed.
imports: Coq.Sorting.Permutation Coq.Classes.EquivDec CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext Coq.Lists.List