employ rewrite in lemma-map-lookupM-assoc