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

[tahina-pro]

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

[tahina-pro]

Thanks Théophile, I mostly agree with you, at least for the definition bodies of those lemmas. Now in practice, if lemmas for both flavors are already used in other F* developments, we shouldn't break existing code, so we might need to keep both lemma names, even though they might all refer to the prop predicate, leveraging a SMTPat on equivalence lemmas between the bool and the prop flavors, as you suggest. In that case, I don't think there would be any significant risk of proof performance degradation.