Further work on lemmas towards mac_message lemma.