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