variant of `measurable_fun_eqr`

it appeared during the conversion of PR #1306 that we might like to have the following lemma:
```coq
Lemma measurable_fun_indic_eqr D f g : measurable_fun D f -> measurable_fun D g ->
  measurable_fun D \1_[set x | f x == g x].
```