redid proofs from SPL refinement theory
renaming incorrectly named definition for stronger PL refinement
populations theory using multisets instead of sets
other compositionality results for multi product lines