proposition: Lemma select_isNondet S (M : nondetStateMonad S) A (s : seq A) : nondetState_isNondet (select s : M _).
proof: Proof. elim: s => [/= | u v [x /= <-]]; first by exists (@ndFail _). by exists (ndAlt (ndRet (u, v)) (ndBind x (fun x => ndRet (x.1, u :: x.2)))). Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib