fact: Definition DM_RC_G6(c : A -> Comp B) := [a, s_A] <-$2 A1; opt_b' <-$ ( b <-$ compMap B_EqDec (fun _ : nat => (c a)) (forNats n); ret head (filter P b)); match opt_b' with | Some b' => A2 s_A b' | None => ret false end.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid