proposition: Theorem OMH_G1_G2_close : | Pr[OMH_G1] - Pr[OMH_G2] | <= (q / 1) * k.
proof: Proof. rewrite OMH_G1_equiv. rewrite OMH_G2_equiv. eapply G1_G2_close; intuition. apply OMH_G_oc_wf. eapply OMH_G_oc_qam. eauto. repeat rewrite Gi_oracleMap_equiv, Gi_oracleMap'_equiv, OMH_G_i_equiv. auto. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF