proposition: Theorem Gi_oracleMap_equiv : forall i, Pr[Gi _ _ O1 O2 A1 OMH_G_oc i] == Pr[Gi_oracleMap i].
proof: Proof. intuition. unfold Gi, OMH_G_oc, Gi_oracleMap. fcf_skip. fcf_simp. fcf_to_prhl_eq. simpl. fcf_inline_first. eapply comp_spec_eq_symm. fcf_skip. eapply compFold_oc_equiv. subst. simpl. fcf_ident_expand_l. fcf_inline_first. fcf_skip. fcf_simp. fcf_spec_ret. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF