proposition: Theorem oc_compMap_wf : forall (A B C D : Set)(eqd : EqDec B)(c : A -> OracleComp C D B) ls, (forall a, In a ls -> well_formed_oc (c a)) -> well_formed_oc (oc_compMap eqd c ls).
proof: Proof. induction ls; intuition; simpl in *; econstructor; wftac; intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.PRF