proposition: Theorem oc_EqDec : forall (A B C: Set), OracleComp A B C -> (A -> B) -> (A -> EqDec B) -> EqDec C.
proof: Proof. induction 1; intuition. eapply pair_EqDec; intuition. eapply IHX; intuition. apply oc_base_exists in X1; intuition. eapply comp_EqDec; intuition. eapply H. eapply oc_base_exists; eauto. intuition. intuition. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec