variant of `measurable_fun_eqr`

[affeldt-aist]

it appeared during the conversion of PR #1306 that we might like to have the following lemma:

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].