fact: Definition genGoodMatch (n : nat) := let fix aux_arb init_size size n := match size with | 0 => backtrack [(1, match n with | 0 => ret (Some Foo1) | _.+1 => ret None end )] | S _ => backtrack [(1, match n with | 0 => ret (Some Foo1) | _.+1 => ret None end)] end in fun sz => aux_arb sz sz n.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads