proposition: Theorem A_NMAC_G1_0_equiv : Pr[A_NMAC] == Pr[A_NMAC_G1_0].
proof: Proof. unfold A_NMAC, A_NMAC_G1_0. inline_first. comp_skip. remember (splitVector c c x) as z. comp_simp. erewrite append_splitVector. reflexivity. trivial. Qed.
imports: FCF PRF SplitVector HMAC_spec