proposition: Lemma finite_inv_list_covers : forall (E:set A), finite E -> exists L, list_covers E L.
proof: Proof. Proof using. introv (L&HN). exists L. intros. applys* HN. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)