proposition: Theorem OMH_G_oc_qam : forall p s, In (s, p) (getSupport A1) -> queries_at_most (OMH_G_oc p) q.
proof: Proof. intuition. unfold OMH_G_oc. econstructor. econstructor. eapply oc_compMap_qam. intuition. econstructor. intuition. econstructor. rewrite Nat.mul_1_r. rewrite Nat.add_0_r. eapply max_queries. eauto. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF