proposition: Lemma slowsort_isNondet s : plus_isNondet (slowsort s : M _).
proof: Proof. rewrite /slowsort kleisliE. have [syn syn_qperm] := @qperm_isNondet M _ s. exists (ndBind syn (fun a => ndBind (if sorted a then ndRet tt else ndFail unit) (fun _ : unit => ndRet a))). rewrite /= syn_qperm; bind_ext => s' /=. case: ifPn => sorteds'. by rewrite /= bindretf assertE sorteds' guardT bindskipf. by rewrite /= assertE (negbTE sorteds') guardF bindfailf. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)