Avoid lemma duplication between `bool` and `prop` predicates

From @TWal in https://github.com/FStarLang/FStar/pull/3094#issuecomment-1810450113 :

> 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 *)
> ```

Start by reviewing the duplicated bool and prop predicates and the ulib lemma named mem_memP, using the discussion linked from PR 3094 as context. Done means determining whether prop-side lemmas plus predicate-equivalence lemmas can replace the bool-side duplicates, potentially through suitable SMT patterns, without losing the relevant deductions.

Written by the indexing model from the issue text.