Commit 2024-06-24 11:40 5bc6aac0

chore: distribute fun_prop tagging of measurability lemmas (#13869) into the respective files: essentially dissolves the FunProp/Measurable and AEMeasurable files. (The latter is kept to note two missing statements. It is not imported anywhere any more.) This is a pre-requisite for #13781, so fun_prop can be used without breaking existing the assert_not_exists statements.