fact: Definition rewindable_P_oracle := forall (A : Set)(eqd : EqDec A), (Commitment -> P_respond_oracle -> Comp (A * bool)) -> forall (B: Set), (A -> Commitment -> P_respond_oracle -> Comp B) -> Comp B.
imports: Crypto FCF RndNat Asymptotic