proposition: Theorem OMH_G_oc_equiv : forall O, Pr[OMH_G O] == Pr[ [s, s_A] <-$2 A1; [b, _] <-$2 (OMH_G_oc s_A) _ _ O s; ret b ].
proof: Proof. intuition. unfold OMH_G, OMH_G_oc. fcf_skip. fcf_simp. fcf_to_prhl_eq. simpl. fcf_inline_first. fcf_skip. apply compFold_oc_equiv. subst. fcf_inline_first. fcf_ident_expand_l. fcf_skip. fcf_simp. fcf_spec_ret. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF