proposition: Lemma uniquify_map A B (d:decidable_eq B)(f:A->B)(l:list A) : exists l', NoDup (map f l') /\ incl (map f l) (map f l').
proof: Proof. induction l as [|a l IHl]. - exists nil. simpl. split; [now constructor | red; trivial]. - destruct IHl as (l' & N & I). destruct (In_decidable d (f a) (map f l')). + exists l'; simpl; split; trivial. intros x [Hx|Hx]. * now subst. * now apply I. + exists (a::l'); simpl; split. * now constructor. * intros x [Hx|Hx]. -- subst; now left. -- right; now apply I. Qed.
imports: List Decidable