Solved last case in base case of mac_message_lemma.
Proved mac_message_lemma.