compositionality with additional conditions defined, only need to finish proof of additional lemma
only missing replace refinement condition and equality of pl1 and pl2 in compositionality theorem
checkpoint before another major review to the theory
only mpl wf and choose lemma left to prove