fact: Fixpoint remove_duplicates A (l:list A) : list A := match l with | nil => nil | x::l' => x :: (remove x (remove_duplicates l')) end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)