Properties of List.Tot.no_repeats_p

[tahina-pro]

This pull request introduces some reasoning principles to prove that a list is (or is not) without repetitions, using the no_repeats_p predicate that does not require the type of list elements to have decidable equality.

Many of those properties already exist for noRepeats (which works only on eqtypes); I replicated those properties for no_repeats_p in this PR.

Regarding no_repeats_p_append_permut with 5 arguments, I expect users to use this lemma with l2 and l4 being singletons; and similarly for l in no_repeats_p_false_intro

[TWal]

The bool and prop properties are causing a lot of redundancy in ulib, but is it needed?
While I agree that we need to define each predicate twice (although it would have been better with some consistent naming convention, e.g. noRepeats vs no_repeats_p, or memP vs no_repeats_p), probably that each lemma could be defined only once?
I feel like we could define lemmas only on the prop predicates, and using a lemma stating the equivalence between bool / prop predicates it would suffice to deduce the lemmas on bool predicates?
Probably that it could even be done automatically with carefully crafted SMT patterns?

The comment above the lemma mem_memP seem to go in this direction

(** Correctness of [mem] for types with decidable equality. TODO:
replace [mem] with [memP] in relevant lemmas and define the right
SMTPat to automatically recover lemmas about [mem] for types with
decidable equality *)

[tahina-pro]

Thanks Théophile for your remark; I opened issue #3095 to this end, which would be solved as a separate, more general PR that would also cover memP, etc.