proposition: Theorem hasDups_inj_equiv : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(lsa : list A)(inj : A -> B), (forall a1 a2, inj a1 = inj a2 -> a1 = a2) -> hasDups _ lsa = hasDups _ (map inj lsa).
proof: Proof. induction lsa; intuition; simpl in *. destruct (in_dec (EqDec_dec eqda) a lsa); destruct (in_dec (EqDec_dec eqdb) (inj a) (map inj lsa)); intuition. exfalso. apply n. apply in_map_iff. econstructor. intuition. apply in_map_iff in i. destruct i. intuition. apply H in H1. subst. intuition. Qed.
imports: FCF.FCF FCF.CompFold ZifyNat