proposition: Theorem G2_5_equiv : Pr[G2_5] == Pr[G2].
proof: Proof. unfold G2_5, G2. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => forall z, arrayLookup _ a z = arrayLookup _ b z)). intuition. intuition. eapply randomFunc_mem_spec. intuition. simpl in *. intuition. subst. comp_simp. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv