Duplicate lemmas `integrable_locally_restrict` and `integrable_locally`

[Yosuke-Ito-345]

These lemmas appear to be exactly the same. Is this intended?

lebesgue_integral_theory/lebesgue_integral_differentiation.v

Lemma integrable_locally_restrict f (A : set R) : measurable A ->
  mu.-integrable A (EFin \o f) -> locally_integrable [set: R] (f \_ A).

ftc.v

Lemma integrable_locally f (A : set R) : measurable A ->
  mu.-integrable A (EFin \o f) -> locally_integrable [set: R] (f \_ A).