fact: Definition GenSizedSuchThateq_manual {A} (y_ : A) := let fix aux_arb (init_size size : nat) (y_0 : A) {struct size} : G (option A) := match size with | 0 => backtrack [(1, returnGen (Some y_0))] | S _ => backtrack [(1, returnGen (Some y_0))] end in fun size => aux_arb size size y_.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads