proposition: Lemma qperm_idempotent : qperm >=> qperm = qperm :> (seq A -> M (seq A)).
proof: Proof. by rewrite -iperm_qperm iperm_idempotent. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)