Tracking issue: try replacing measurability by fun_prop

[grunweg]

In #13770, I replaced several very slow measurability calls by the equivalent proofs. This automation should be re-instated: either by speeding up aesop or, perhaps better, by making the much faster tactic fun_prop work in these situations and using it instead.
In fact, this branch manages to use mostly use fun_prop in these places: it's worth investigating if further measurability calls can and should be replaced.