proposition: Lemma remove_duplicates_eq : forall A (cmp:A->A->bool) (l:list A), is_beq cmp -> remove_duplicates cmp l = LibList.remove_duplicates l.
proof: Proof. Proof using. Local Transparent LibList.remove_duplicates. introv E. induction l as [|x l']; simpl; fequals. rewrite* remove_eq. congruence. Qed.
imports: TLC(LibTactics LibReflect)