Finished monadic associativity lemma, though with the requirement that
the new variable is fresh.