fixing some issues on formalization of MPLs
fixed am refinement compositionality proof and working on refactoring the MPL theory