`NoDup_dec` definition is opaque

[olympichek]

The decidability of the NoDup predicate (NoDup_dec) is defined with Qed instead of Defined, which makes it opaque and thus makes it impossible to compute with it.

For example, other proofs of decidability of list operations (e.g. in_dec or list_eq_dec) are defined as transparent.