proposition: Lemma refin_ret_iperm (M : plusMonad) (A : UU0) (s : seq A) : (Ret s : M _) `<=` iperm s.
proof: Proof. by case: (@iperm_is_alt_ret M _ s) => m ->; rewrite /refin altA altmm. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)