proposition: Theorem OMH_G_oc_wf : forall p, well_formed_oc (OMH_G_oc p).
proof: Proof. intuition. econstructor. apply oc_compMap_wf. intuition. econstructor. intuition. econstructor. auto. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF