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