sorted out compositionality with additional axioms - have to check with Paulo
worked out compositionality with additional lemmas and definition - to check with Paulo