proposition: Lemma refin_qperm_ret (M : plusMonad) (A : eqType) (s : seq A) : (Ret s : M _) `<=` qperm s.
proof: Proof. by rewrite -iperm_qperm; exact: refin_ret_iperm. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)