made the definition of mSSubstAux more concise.
some proofs broke as a result. took ~1 hour to fix them all.