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