proposition: Theorem Permutation_hasDups : forall (A : Set)(eqd : EqDec A)(ls1 ls2 : list A), Permutation ls1 ls2 -> hasDups eqd ls1 = hasDups eqd ls2.
proof: Proof. intuition. case_eq ( hasDups eqd ls1); intuition. apply hasDups_true_not_NoDup in H0. intuition. case_eq (hasDups eqd ls2); intuition. apply hasDups_false_NoDup in H1; intuition. exfalso. eapply H0. eapply permutation_NoDup. eapply Permutation_sym. eauto. trivial. eapply hasDups_false_NoDup in H0; intuition. case_eq (hasDups eqd ls2); intuition. apply hasDups_true_not_NoDup in H1. exfalso. apply H1. eapply permutation_NoDup; eauto. Qed.
imports: FCF.FCF FCF.CompFold ZifyNat Permutation