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