mac_message_lemma finally complete, cleaned up unneeded lemmas.
Clean up, all proofs work, more restrictive types in uccom.