proposition: Theorem oracleMap_wf : forall (D R S : Set)(eqds : EqDec S)(eqdr : EqDec R) (oracle : S -> D -> Comp (R * S))ds s, (forall s x, well_formed_comp (oracle s x)) -> well_formed_comp (@oracleMap D R S _ _ oracle s ds).
proof: Proof. intuition. unfold oracleMap. eapply compFold_wf; intuition. wftac. Qed.
imports: FCF.FCF FCF.CompFold FCF.Array FCF.Hybrid