fact: Definition goodFooNarrow_decOpt (n_ : nat) (foo_ : Foo) := let fix aux_arb (init_size size0 n_0 : nat) (foo_0 : Foo) : option bool := match size0 with | 0 => checker_backtrack [(fun _ : unit => match foo_0 with | Foo1 => Some true | _ => Some false end) ; (fun _ : unit => None)] | size'.+1 => checker_backtrack [(fun _ : unit => match foo_0 with | Foo1 => Some true | _ => Some false end) ; (fun _ : unit => match aux_arb init_size size' 0 foo_0 with | Some true => match aux_arb init_size size' 1 foo_0 with | Some true => Some true | Some false => Some false | None => None end | Some false => Some false | None => None end)] end in fun size0 : nat => aux_arb size0 size0 n_ foo_.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads