Proof strategy: show that a list satisfies no-duplicatesp-equal because it has no element whose duplicity is over 1.
This is often a good way to prove no-duplicatesp. This is a
basic pick-a-point style theorem that you can (manually)
Theorem:
(defthm duplicity-constraint (implies (duplicity-hyp) (equal (duplicity a (duplicity-lhs)) (duplicity a (duplicity-rhs)))))
Theorem:
(defthm no-duplicatesp-equal-same-by-duplicity (implies (duplicity-hyp) (equal (no-duplicatesp-equal (duplicity-lhs)) (no-duplicatesp-equal (duplicity-rhs)))))