fact: Definition list_covers A (E:set A) (L:list A) := forall x, x \in E -> mem x L.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)