proposition: Lemma goodFooNarrow_decOpt_correct n foo : goodFooNarrow_decOpt n foo = @decOpt (goodFooNarrow n foo) _.
proof: Proof. reflexivity. Qed.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads