proposition: Lemma iperm_qperm : @iperm M A = @qperm M A.
proof: Proof. rewrite boolp.funeqE => s. apply qperm_elim => [//|h t ihys ihzs]. rewrite iperm_cons_splits splits_bseqE fmapE bindA. bind_ext => -[a b]; rewrite bindretf. by rewrite (ihys (a, b) _ b) (ihzs (a, b) a). Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)