proposition: Theorem OMH_G1_equiv: Pr[OMH_G1] == Pr[G1 _ O1 A1 OMH_G_oc].
proof: Proof. unfold OMH_G1. rewrite OMH_G_oc_equiv. unfold G1, OMH_G_oc. reflexivity. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF