proposition: Theorem oc_base_exists : forall (A B C : Set), OracleComp A B C -> (A -> B) -> C.
proof: Proof. induction 1; intuition; simpl in *. eapply comp_base_exists; intuition. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec