proposition: Theorem G0_1_equiv : Pr[PRF_G_A ({0, 1}^(c + k)) hF _ A] == Pr[G0_1].
proof: Proof. unfold PRF_G_A, G0_1. inline_first. comp_skip. unfold f_oracle, hF. remember (splitVector c k x) as z. comp_simp. reflexivity. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv