measurable_sfunP does not refer to sfun

[t6s]

analysis/theories/lebesgue_integral.v

Lines 156 to 157 in 89fb9d2

	Lemma measurable_sfunP {d d'} {aT : measurableType d} {rT : measurableType d'}
	(f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y).

lebesgue_integral.measurable_sfunP looks like irrelevant to sfun. Typo either in the name or the statement?

[t6s]

TODO: test changing Lemma to Let and see CI results