fact: Definition oracleMap(D R S: Set)(eqds : EqDec S)(eqdr : EqDec R)(oracle : (S * D) -> Comp (S * R))(s : S)(ds : list D) := compFold _ (fun acc d => [s, r] <-$2 oracle (fst acc, d); ret (fst acc, snd acc ++ r :: nil)) (s, nil) ds.
imports: Crypto Permutation CompFold Array FCF State