of the Lebesgue scheme that is now obsolete.

Add new Mp for full Rbar functions (still admitted).

chain: simple_fun -> Mp -> Lint_p.

(Could be moved to simple_fun.v and measurable_fun.v.)

Add measurability or not?

(This is presumably its only application.)

Define meas_swap and prove LInt_p_swap by using LInt_p_meas_image.