Define NoDup_dec with Defined instead of Qed

[olympichek]

This pull request will close issue #125

[proux01]

@rocq-prover/stdlib-maintainers could anyone have a look please (I'm not qualified myself about those transparencies questions, their impact in terms of performances,...)

[ppedrot]

I think this is a very bad idea. It exposes bits of proofs constructed via tactics and that's a big no-no. Furthermore it's probably not usable in practice due to these huge proof terms creeping in.

Across the decades we've been taking nonsense design decisions in the stdlib out of inertia, but the proper way to do this is to write a decision function returning a boolean and prove that indeed it reflects the predicate.