New (empty) file measurable_R.v that will replace sigma_algebra_R_Rbar.v.

Diff' -> Compl_loc
_iff -> _equiv