proposition: Lemma qperm_partl_cons (p x : E) (ys zs xs : seq E) : qperm_partl p ys zs (x :: xs) = dispatch_Ret x p (ys, zs, xs) >>= uncurry3 (qperm_partl p).
proof: Proof. by rewrite /=; case: ifPn => xp; rewrite bindA; under [RHS]eq_bind do rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)