proposition: Lemma noduplicates_eq : forall A (cmp:A->A->bool) (l:list A), is_beq cmp -> noduplicates cmp l = isTrue (LibList.noduplicates l).
proof: Proof. Proof using. introv E. extens. induction l as [|x l']; simpl; rew_listx; rew_bool_eq in *. { autos*. } { rewrite* mem_eq. rew_bool_eq. iff (M1&M2); splits*. } Qed.
imports: TLC(LibTactics LibReflect)