fact: Fixpoint randomFunc_eager_arr(allD : list D) := match allD with | nil => ret nil | d :: allD' => arr' <-$ randomFunc_eager_arr allD'; r <-$ RndR; ret ((d, r) :: arr') end.
imports: Crypto Permutation CompFold Array FCF State