fact: Definition to_set (xs : list A) : set A := set_st (fun x => mem x xs).
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)