proposition: Lemma mem_remove_duplicates : forall x l, mem x (remove_duplicates l) = mem x l.
proof: Proof. Proof using. introv. extens. repeat rewrite <- Mem_mem. apply~ remove_duplicates_spec. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)