proposition: Lemma qperm_cons x xs : qperm (x :: xs) = splits xs >>= (fun '(ys, zs) => liftM2 (fun a b => a ++ x :: b) (qperm ys) (qperm zs)).
proof: Proof. rewrite qperm_equation_2 splits_bseqE fmapE bindA; bind_ext => -[? ?]. by rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)