proposition: Lemma EnumCovered_strengthen: forall U A B, Included A B -> EnumCovered U B -> EnumCovered U A.
proof: Proof. intros. destruct X as [x ?H]. exists x. split; [tauto |]. intros. apply H in H1. firstorder. Qed.
imports: Coq.Sorting.Permutation Coq.Classes.EquivDec CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext Coq.Lists.List