fact: Fixpoint BoundedRepeat (A : Set)(eqd : EqDec A)(n : nat)(c : Comp A)(P : A -> bool)(def : A) := match n with | O => ret (def) | S n' => (Bind c (fun x => if (P x) then (ret x) else (BoundedRepeat _ n' c P def))) end.
imports: Crypto FCF RndNat Asymptotic