feat(data/list/duplicate): prop that element is a duplicate (#7824)
As discussed in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nodup.20and.20decidability and #7587
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>