proposition: Lemma iperm_is_alt_ret s : exists m, iperm s = Ret s [~] m :> M _.
proof: Proof. elim: s => [|h t [m ih] /=]; first by exists fail; rewrite altmfail. case: (@insert_Ret M A h t) => n Hn. by eexists; rewrite ih alt_bindDl bindretf Hn -altA. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)