proposition: Lemma qperm_partl_isNondet p (s a b : seq E) : plus_isNondet (qperm_partl p a b s).
proof: Proof. elim: s p a b => [p a b|h t ih p a b /=]; first by exists (ndRet (a, b)). case: ifPn => hp. have [syn synE] := @qperm_isNondet M _ b. exists (ndBind syn (fun zs' => sval (ih p (rcons a h) zs'))) => /=. by rewrite synE /=; bind_ext => ? /=; case: ih. have [syn synE] := @qperm_isNondet M _ (rcons b h). exists (ndBind syn (fun zs' => sval (ih p a zs'))) => /=. by rewrite synE /=; bind_ext => ? /=; case: ih. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)