fact: Fixpoint oc_compMap(A B C D : Set)(eqdb : EqDec B)(c : A -> OracleComp C D B)(ls : list A) : OracleComp C D (list B) := match ls with | nil => $ (ret nil) | a :: ls' => b <--$ c a; lsb' <--$ oc_compMap _ c ls'; $ (ret (b :: lsb')) end.
imports: FCF.FCF FCF.CompFold FCF.Hybrid